Theorem mp3an3 1561

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	⊢ 𝜒
mp3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1114	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 20	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 383  df-3an 1073

This theorem is referenced by:  mp3an13  1563  mp3an23  1564  mp3anl3  1568  opelxp  5286  ov  6927  ovmpt2a  6938  ovmpt2  6943  oaword1  7786  oneo  7815  oeoalem  7830  oeoelem  7832  nnaword1  7863  nnneo  7885  erov  7997  enrefg  8141  f1imaen  8171  mapxpen  8282  acnlem  9071  cdacomen  9205  infmap  9600  canthnumlem  9672  tskin  9783  tsksn  9784  tsk0  9787  gruxp  9831  gruina  9842  genpprecl  10025  addsrpr  10098  mulsrpr  10099  supsrlem  10134  mulid1  10239  00id  10413  mul02lem1  10414  ltneg  10730  leneg  10733  suble0  10744  div1  10918  nnaddcl  11244  nnmulcl  11245  nnge1  11248  nnsub  11261  2halves  11462  halfaddsub  11467  addltmul  11470  zleltp1  11630  nnaddm1cl  11636  zextlt  11653  eluzp1p1  11914  uzaddcl  11946  znq  11995  xrre  12205  xrre2  12206  fzshftral  12635  fraclt1  12811  expadd  13109  expmul  13112  expubnd  13128  sqmul  13133  bernneq  13197  faclbnd2  13282  faclbnd6  13290  hashgadd  13368  hashun2  13374  hashssdif  13402  hashfun  13426  ccatlcan  13681  ccatrcan  13682  shftval3  14024  sqrlem1  14191  caubnd2  14305  bpoly2  14994  bpoly3  14995  fsumcube  14997  efexp  15037  efival  15088  cos01gt0  15127  odd2np1  15273  halfleoddlt  15294  omoe  15296  opeo  15297  divalglem5  15328  gcdmultiple  15477  sqgcd  15486  nn0seqcvgd  15491  phiprmpw  15688  eulerthlem2  15694  odzcllem  15704  pythagtriplem15  15741  pythagtriplem17  15743  pcelnn  15781  4sqlem3  15861  xpscfn  16427  fullfunc  16773  fthfunc  16774  prfcl  17051  curf1cl  17076  curfcl  17080  hofcl  17107  odinv  18185  lsmelvalix  18263  dprdval  18610  lsp0  19222  lss0v  19229  coe1scl  19872  zndvds0  20114  frlmlbs  20353  lindfres  20379  lmisfree  20398  ntrin  21086  lpsscls  21166  restperf  21209  txuni2  21589  txopn  21626  elqtop2  21725  xkocnv  21838  ptcmp  22082  xblpnfps  22420  xblpnf  22421  bl2in  22425  unirnblps  22444  unirnbl  22445  blpnfctr  22461  dscopn  22598  bcthlem4  23343  minveclem2  23416  minveclem4  23422  icombl  23552  i1fadd  23682  i1fmul  23683  dvn1  23909  dvexp3  23961  plyconst  24182  plyid  24185  sincosq1eq  24485  sinord  24501  cxpp1  24647  cxpsqrtlem  24669  cxpsqrt  24670  angneg  24754  dcubic  24794  issqf  25083  ppiub  25150  bposlem1  25230  bposlem2  25231  bposlem9  25238  axlowdimlem6  26048  axlowdimlem14  26056  axcontlem2  26066  structgrssvtxlemOLD  26136  pthdlem2  26899  0ewlk  27294  ipasslem1  28026  ipasslem2  28027  ipasslem11  28035  minvecolem2  28071  minvecolem3  28072  minvecolem4  28076  shsva  28519  h1datomi  28780  lnfnmuli  29243  leopsq  29328  nmopleid  29338  opsqrlem6  29344  pjnmopi  29347  hstle  29429  csmdsymi  29533  atcvatlem  29584  dpfrac1  29939  dpfrac1OLD  29940  elsx  30597  dya2iocnrect  30683  cvmliftphtlem  31637  wlimeq12  32101  frecseq123  32114  nosupno  32186  nosupfv  32189  scutval  32248  scutun12  32254  fvray  32585  fvline  32588  tailfb  32709  uncov  33723  tan2h  33734  matunitlindflem1  33738  matunitlindflem2  33739  poimirlem32  33774  mblfinlem4  33782  mbfresfi  33788  mbfposadd  33789  itg2addnc  33796  ftc1anclem5  33821  ftc1anclem8  33824  dvasin  33828  heiborlem7  33948  igenidl  34194  el3v3  34335  atlatmstc  35128  dihglblem2N  37104  eldioph4b  37901  diophren  37903  rmxp1  38023  rmyp1  38024  rmxm1  38025  rmym1  38026  wepwso  38139  pfx2  41940  dig0  42928  onetansqsecsq  43033  cotsqcscsq  43034