Theorem mp3an2 1451

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 1118	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
4	1, 3	mpanl2 701	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mp3anl2  1458  vtoclegft  3551  tz7.7  6347  ordin  6351  onfr  6360  fprresex  8267  tfrlem11  8334  phplem2  9147  epfrs  9663  zorng  10436  tsk2  10697  tskcard  10713  gruina  10750  muladd11  11323  00id  11328  ltaddneg  11369  negsub  11449  subneg  11450  muleqadd  11801  diveq0  11826  diveq1  11846  conjmul  11878  recp1lt1  12060  nnsub  12209  addltmul  12397  nnunb  12417  zltp1le  12562  gtndiv  12590  eluzp1m1  12798  zbtwnre  12884  rebtwnz  12885  xnn0le2is012  13185  supxrbnd  13267  divelunit  13434  fznatpl1  13518  flbi2  13758  fldiv  13801  modid  13837  modm1p1mod0  13866  fzen2  13913  nn0ennn  13923  seqshft2  13972  seqf1olem1  13985  ser1const  14002  sq01  14169  expnbnd  14176  faclbnd3  14236  faclbnd5  14242  hashunsng  14336  hashunsngx  14337  hashxplem  14377  ccatrid  14531  ccats1val1  14570  ccat2s1fst  14583  sgnn  15038  01sqrexlem2  15187  01sqrexlem7  15192  leabs  15243  abs2dif  15277  cvgrat  15827  cos2t  16124  sin01gt0  16136  cos01gt0  16137  demoivre  16146  demoivreALT  16147  rpnnen2lem5  16164  rpnnen2lem12  16171  omeo  16314  gcd0id  16467  sqgcd  16510  expgcd  16511  isprm3  16631  eulerthlem2  16730  pczpre  16796  pcrec  16807  ressress  17195  mulgm1  19010  unitgrpid  20307  mdet0pr  22514  m2detleib  22553  cmpcov2  23312  ufileu  23841  tgpconncompeqg  24034  itg2ge0  25671  mdegldg  26006  abssinper  26465  ppiub  27150  chtub  27158  bposlem2  27231  lgs1  27287  cofcutr  27874  addsbday  27966  negsbdaylem  28004  precsexlem10  28160  onscutlt  28207  n0sbday  28286  bdayn0p1  28300  eucliddivs  28307  nnzs  28316  zzs12  28389  remulscllem1  28406  colinearalglem4  28891  axsegconlem1  28899  axpaschlem  28922  axcontlem2  28947  axcontlem4  28949  axcontlem7  28952  axcontlem8  28953  funvtxval  29000  funiedgval  29001  vc0  30555  vcm  30557  nvmval2  30624  nvmf  30626  nvmdi  30629  nvnegneg  30630  nvpncan2  30634  nvaddsub4  30638  nvm1  30646  nvdif  30647  nvpi  30648  nvz0  30649  nvmtri  30652  nvabs  30653  nvge0  30654  imsmetlem  30671  4ipval2  30689  ipval3  30690  ipidsq  30691  dipcj  30695  sspmval  30714  ipasslem1  30812  ipasslem2  30813  dipsubdir  30829  hvsubdistr1  31030  shsubcl  31201  shsel3  31296  shunssi  31349  hosubdi  31789  lnopmi  31981  nmophmi  32012  nmopcoi  32076  opsqrlem6  32126  hstle  32211  hst0  32214  mdsl2i  32303  superpos  32335  dmdbr5ati  32403  f1rnen  32605  resvsca  33299  pthhashvtx  35110  cvmliftphtlem  35299  topdifinffinlem  37330  finixpnum  37594  tan2h  37601  poimirlem3  37612  poimirlem4  37613  poimirlem7  37616  poimirlem16  37625  poimirlem17  37626  poimirlem19  37628  poimirlem20  37629  poimirlem24  37633  poimirlem28  37637  mblfinlem2  37647  mblfinlem4  37649  ismblfin  37650  el3v2  38208  atlatle  39308  pmaple  39750  dihglblem2N  41283  sn-ltaddneg  42437  elnnrabdioph  42790  rabren3dioph  42798  zindbi  42930  expgrowth  44319  binomcxplemnotnn0  44340  trelpss  44439  etransc  46276  mogoldbb  47781  pgrple2abl  48348  aacllem  49785