Theorem mp3an2 1478

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

Hypotheses

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

Assertion

Ref	Expression
mp3an2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an2

Step	Hyp	Ref	Expression
1		mp3an2.1	. 2 ⊢ 𝜓
2		mp3an2.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expa 1136	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 714	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3anl2  1485  vtoclegft  3546  tz7.7  6387  ordin  6392  onfr  6401  fprresex  8313  tfrlem11  8381  phplem2  9203  epfrs  9714  zorng  10510  tsk2  10778  tskcard  10794  gruina  10831  muladd11  11408  00id  11413  ltaddneg  11454  negsub  11534  subneg  11535  muleqadd  11886  diveq0  11910  diveq1  11929  conjmul  11960  recp1lt1  12141  nnsub  12308  addltmul  12508  nnunb  12528  zltp1le  12672  gtndiv  12702  eluzp1m1  12917  zbtwnre  12999  rebtwnz  13000  xnn0le2is012  13302  supxrbnd  13384  divelunit  13551  fznatpl1  13637  flbi2  13882  fldiv  13925  modid  13961  modm1p1mod0  13990  fzen2  14037  nn0ennn  14047  seqshft2  14096  seqf1olem1  14109  ser1const  14126  sq01  14293  expnbnd  14300  faclbnd3  14360  faclbnd5  14366  hashunsng  14460  hashunsngx  14461  hashxplem  14502  ccatrid  14657  ccats1val1  14698  ccat2s1fst  14711  sgnn  15171  01sqrexlem2  15334  01sqrexlem7  15339  leabs  15390  abs2dif  15424  cvgrat  15976  cos2t  16272  sin01gt0  16284  cos01gt0  16285  demoivre  16294  demoivreALT  16295  rpnnen2lem5  16312  rpnnen2lem12  16319  omeo  16462  gcd0id  16615  sqgcd  16658  expgcd  16659  isprm3  16779  eulerthlem2  16879  pczpre  16945  pcrec  16956  ressress  17345  mulgm1  19223  unitgrpid  20532  mdet0pr  22820  m2detleib  22859  cmpcov2  23621  ufileu  24151  tgpconncompeqg  24344  itg2ge0  25969  mdegldg  26298  abssinper  26766  ppiub  27448  chtub  27456  bposlem2  27529  lgs1  27585  cofcutr  28197  addbday  28291  negbdaylem  28329  precsexlem10  28489  oncutlt  28537  n0bday  28625  bdayn0p1  28642  eucliddivs  28649  nnzs  28659  bdaypw2n0bndlem  28736  zz12s  28748  remulscllem1  28773  colinearalglem4  29374  axsegconlem1  29382  axpaschlem  29405  axcontlem2  29430  axcontlem4  29432  axcontlem7  29435  axcontlem8  29436  funvtxval  29483  funiedgval  29484  pthhashvtx  30202  vc0  31063  vcm  31065  nvmval2  31132  nvmf  31134  nvmdi  31137  nvnegneg  31138  nvpncan2  31142  nvaddsub4  31146  nvm1  31154  nvdif  31155  nvpi  31156  nvz0  31157  nvmtri  31160  nvabs  31161  nvge0  31162  imsmetlem  31179  4ipval2  31197  ipval3  31198  ipidsq  31199  dipcj  31203  sspmval  31222  ipasslem1  31320  ipasslem2  31321  dipsubdir  31337  hvsubdistr1  31538  shsubcl  31709  shsel3  31804  shunssi  31857  hosubdi  32297  lnopmi  32489  nmophmi  32520  nmopcoi  32584  opsqrlem6  32634  hstle  32719  hst0  32722  mdsl2i  32811  superpos  32843  dmdbr5ati  32911  f1rnen  33109  resvsca  33780  noinfepfnregs  35666  cvmliftphtlem  35904  topdifinffinlem  38109  finixpnum  38367  tan2h  38374  poimirlem3  38380  poimirlem4  38381  poimirlem7  38384  poimirlem16  38393  poimirlem17  38394  poimirlem19  38396  poimirlem20  38397  poimirlem24  38401  poimirlem28  38405  mblfinlem2  38415  mblfinlem4  38417  ismblfin  38418  el3v2  38987  atlatle  40201  pmaple  40642  dihglblem2N  42175  sn-ltaddneg  43350  elnnrabdioph  43656  rabren3dioph  43664  zindbi  43795  expgrowth  45167  binomcxplemnotnn0  45188  trelpss  45285  etransc  47119  mogoldbb  48709  pgrple2abl  49303  aacllem  50780