Theorem mp3an2 1449

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 700	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  mp3anl2  1456  vtoclegft  3601  tz7.7  6421  ordin  6425  onfr  6434  fprresex  8351  wfrlem14OLD  8378  wfrlem17OLD  8381  tfrlem11  8444  phplem2  9271  epfrs  9800  zorng  10573  tsk2  10834  tskcard  10850  gruina  10887  muladd11  11460  00id  11465  ltaddneg  11505  negsub  11584  subneg  11585  muleqadd  11934  diveq0  11959  diveq1  11979  conjmul  12011  recp1lt1  12193  nnsub  12337  addltmul  12529  nnunb  12549  zltp1le  12693  gtndiv  12720  eluzp1m1  12929  zbtwnre  13011  rebtwnz  13012  xnn0le2is012  13308  supxrbnd  13390  divelunit  13554  fznatpl1  13638  flbi2  13868  fldiv  13911  modid  13947  modm1p1mod0  13973  fzen2  14020  nn0ennn  14030  seqshft2  14079  seqf1olem1  14092  ser1const  14109  sq01  14274  expnbnd  14281  faclbnd3  14341  faclbnd5  14347  hashunsng  14441  hashunsngx  14442  hashxplem  14482  ccatrid  14635  ccats1val1  14674  ccat2s1fst  14687  sgnn  15143  01sqrexlem2  15292  01sqrexlem7  15297  leabs  15348  abs2dif  15381  cvgrat  15931  cos2t  16226  sin01gt0  16238  cos01gt0  16239  demoivre  16248  demoivreALT  16249  rpnnen2lem5  16266  rpnnen2lem12  16273  omeo  16414  gcd0id  16565  sqgcd  16609  expgcd  16610  isprm3  16730  eulerthlem2  16829  pczpre  16894  pcrec  16905  ressress  17307  mulgm1  19134  unitgrpid  20411  mdet0pr  22619  m2detleib  22658  cmpcov2  23419  ufileu  23948  tgpconncompeqg  24141  itg2ge0  25790  mdegldg  26125  abssinper  26581  ppiub  27266  chtub  27274  bposlem2  27347  lgs1  27403  cofcutr  27976  addsbday  28068  negsbdaylem  28106  precsexlem10  28258  n0sbday  28372  nnzs  28390  pw2bday  28436  zzs12  28441  remulscllem1  28450  colinearalglem4  28942  axsegconlem1  28950  axpaschlem  28973  axcontlem2  28998  axcontlem4  29000  axcontlem7  29003  axcontlem8  29004  funvtxval  29053  funiedgval  29054  vc0  30606  vcm  30608  nvmval2  30675  nvmf  30677  nvmdi  30680  nvnegneg  30681  nvpncan2  30685  nvaddsub4  30689  nvm1  30697  nvdif  30698  nvpi  30699  nvz0  30700  nvmtri  30703  nvabs  30704  nvge0  30705  imsmetlem  30722  4ipval2  30740  ipval3  30741  ipidsq  30742  dipcj  30746  sspmval  30765  ipasslem1  30863  ipasslem2  30864  dipsubdir  30880  hvsubdistr1  31081  shsubcl  31252  shsel3  31347  shunssi  31400  hosubdi  31840  lnopmi  32032  nmophmi  32063  nmopcoi  32127  opsqrlem6  32177  hstle  32262  hst0  32265  mdsl2i  32354  superpos  32386  dmdbr5ati  32454  f1rnen  32648  resvsca  33321  pthhashvtx  35095  cvmliftphtlem  35285  topdifinffinlem  37313  finixpnum  37565  tan2h  37572  poimirlem3  37583  poimirlem4  37584  poimirlem7  37587  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem24  37604  poimirlem28  37608  mblfinlem2  37618  mblfinlem4  37620  ismblfin  37621  el3v2  38179  atlatle  39276  pmaple  39718  dihglblem2N  41251  sn-ltaddneg  42418  elnnrabdioph  42763  rabren3dioph  42771  zindbi  42903  expgrowth  44304  binomcxplemnotnn0  44325  trelpss  44424  etransc  46204  mogoldbb  47659  pgrple2abl  48090  aacllem  48895