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  3539  tz7.7  6332  ordin  6336  onfr  6345  fprresex  8240  tfrlem11  8307  phplem2  9114  epfrs  9621  zorng  10395  tsk2  10656  tskcard  10672  gruina  10709  muladd11  11283  00id  11288  ltaddneg  11329  negsub  11409  subneg  11410  muleqadd  11761  diveq0  11786  diveq1  11806  conjmul  11838  recp1lt1  12020  nnsub  12169  addltmul  12357  nnunb  12377  zltp1le  12522  gtndiv  12550  eluzp1m1  12758  zbtwnre  12844  rebtwnz  12845  xnn0le2is012  13145  supxrbnd  13227  divelunit  13394  fznatpl1  13478  flbi2  13721  fldiv  13764  modid  13800  modm1p1mod0  13829  fzen2  13876  nn0ennn  13886  seqshft2  13935  seqf1olem1  13948  ser1const  13965  sq01  14132  expnbnd  14139  faclbnd3  14199  faclbnd5  14205  hashunsng  14299  hashunsngx  14300  hashxplem  14340  ccatrid  14495  ccats1val1  14534  ccat2s1fst  14547  sgnn  15001  01sqrexlem2  15150  01sqrexlem7  15155  leabs  15206  abs2dif  15240  cvgrat  15790  cos2t  16087  sin01gt0  16099  cos01gt0  16100  demoivre  16109  demoivreALT  16110  rpnnen2lem5  16127  rpnnen2lem12  16134  omeo  16277  gcd0id  16430  sqgcd  16473  expgcd  16474  isprm3  16594  eulerthlem2  16693  pczpre  16759  pcrec  16770  ressress  17158  mulgm1  19007  unitgrpid  20303  mdet0pr  22507  m2detleib  22546  cmpcov2  23305  ufileu  23834  tgpconncompeqg  24027  itg2ge0  25663  mdegldg  25998  abssinper  26457  ppiub  27142  chtub  27150  bposlem2  27223  lgs1  27279  cofcutr  27868  addsbday  27960  negsbdaylem  27998  precsexlem10  28154  onscutlt  28201  n0sbday  28280  bdayn0p1  28294  eucliddivs  28301  nnzs  28310  zzs12  28385  remulscllem1  28402  colinearalglem4  28887  axsegconlem1  28895  axpaschlem  28918  axcontlem2  28943  axcontlem4  28945  axcontlem7  28948  axcontlem8  28949  funvtxval  28996  funiedgval  28997  vc0  30554  vcm  30556  nvmval2  30623  nvmf  30625  nvmdi  30628  nvnegneg  30629  nvpncan2  30633  nvaddsub4  30637  nvm1  30645  nvdif  30646  nvpi  30647  nvz0  30648  nvmtri  30651  nvabs  30652  nvge0  30653  imsmetlem  30670  4ipval2  30688  ipval3  30689  ipidsq  30690  dipcj  30694  sspmval  30713  ipasslem1  30811  ipasslem2  30812  dipsubdir  30828  hvsubdistr1  31029  shsubcl  31200  shsel3  31295  shunssi  31348  hosubdi  31788  lnopmi  31980  nmophmi  32011  nmopcoi  32075  opsqrlem6  32125  hstle  32210  hst0  32213  mdsl2i  32302  superpos  32334  dmdbr5ati  32402  f1rnen  32610  resvsca  33297  pthhashvtx  35172  cvmliftphtlem  35361  topdifinffinlem  37391  finixpnum  37644  tan2h  37651  poimirlem3  37662  poimirlem4  37663  poimirlem7  37666  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem24  37683  poimirlem28  37687  mblfinlem2  37697  mblfinlem4  37699  ismblfin  37700  el3v2  38265  atlatle  39418  pmaple  39859  dihglblem2N  41392  sn-ltaddneg  42546  elnnrabdioph  42899  rabren3dioph  42907  zindbi  43038  expgrowth  44427  binomcxplemnotnn0  44448  trelpss  44546  etransc  46380  mogoldbb  47884  pgrple2abl  48464  aacllem  49901