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  8312  tfrlem11  8380  phplem2  9202  epfrs  9713  zorng  10509  tsk2  10777  tskcard  10793  gruina  10830  muladd11  11407  00id  11412  ltaddneg  11453  negsub  11533  subneg  11534  muleqadd  11885  diveq0  11909  diveq1  11928  conjmul  11959  recp1lt1  12140  nnsub  12307  addltmul  12507  nnunb  12527  zltp1le  12671  gtndiv  12701  eluzp1m1  12916  zbtwnre  12998  rebtwnz  12999  xnn0le2is012  13300  supxrbnd  13382  divelunit  13549  fznatpl1  13635  flbi2  13880  fldiv  13923  modid  13959  modm1p1mod0  13988  fzen2  14035  nn0ennn  14045  seqshft2  14094  seqf1olem1  14107  ser1const  14124  sq01  14291  expnbnd  14298  faclbnd3  14358  faclbnd5  14364  hashunsng  14458  hashunsngx  14459  hashxplem  14500  ccatrid  14655  ccats1val1  14696  ccat2s1fst  14709  sgnn  15169  01sqrexlem2  15332  01sqrexlem7  15337  leabs  15388  abs2dif  15422  cvgrat  15974  cos2t  16270  sin01gt0  16282  cos01gt0  16283  demoivre  16292  demoivreALT  16293  rpnnen2lem5  16310  rpnnen2lem12  16317  omeo  16460  gcd0id  16613  sqgcd  16656  expgcd  16657  isprm3  16777  eulerthlem2  16877  pczpre  16943  pcrec  16954  ressress  17343  mulgm1  19218  unitgrpid  20527  mdet0pr  22815  m2detleib  22854  cmpcov2  23616  ufileu  24146  tgpconncompeqg  24339  itg2ge0  25964  mdegldg  26293  abssinper  26756  ppiub  27438  chtub  27446  bposlem2  27519  lgs1  27575  cofcutr  28187  addbday  28281  negbdaylem  28319  precsexlem10  28479  oncutlt  28527  n0bday  28615  bdayn0p1  28632  eucliddivs  28639  nnzs  28649  bdaypw2n0bndlem  28726  zz12s  28738  remulscllem1  28763  colinearalglem4  29352  axsegconlem1  29360  axpaschlem  29383  axcontlem2  29408  axcontlem4  29410  axcontlem7  29413  axcontlem8  29414  funvtxval  29461  funiedgval  29462  pthhashvtx  30180  vc0  31041  vcm  31043  nvmval2  31110  nvmf  31112  nvmdi  31115  nvnegneg  31116  nvpncan2  31120  nvaddsub4  31124  nvm1  31132  nvdif  31133  nvpi  31134  nvz0  31135  nvmtri  31138  nvabs  31139  nvge0  31140  imsmetlem  31157  4ipval2  31175  ipval3  31176  ipidsq  31177  dipcj  31181  sspmval  31200  ipasslem1  31298  ipasslem2  31299  dipsubdir  31315  hvsubdistr1  31516  shsubcl  31687  shsel3  31782  shunssi  31835  hosubdi  32275  lnopmi  32467  nmophmi  32498  nmopcoi  32562  opsqrlem6  32612  hstle  32697  hst0  32700  mdsl2i  32789  superpos  32821  dmdbr5ati  32889  f1rnen  33088  resvsca  33759  noinfepfnregs  35645  cvmliftphtlem  35883  topdifinffinlem  38088  finixpnum  38346  tan2h  38353  poimirlem3  38359  poimirlem4  38360  poimirlem7  38363  poimirlem16  38372  poimirlem17  38373  poimirlem19  38375  poimirlem20  38376  poimirlem24  38380  poimirlem28  38384  mblfinlem2  38394  mblfinlem4  38396  ismblfin  38397  el3v2  38966  atlatle  40180  pmaple  40621  dihglblem2N  42154  sn-ltaddneg  43329  elnnrabdioph  43635  rabren3dioph  43643  zindbi  43774  expgrowth  45146  binomcxplemnotnn0  45167  trelpss  45264  etransc  47098  mogoldbb  48688  pgrple2abl  49282  aacllem  50759