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  3543  tz7.7  6378  ordin  6383  onfr  6392  fprresex  8307  tfrlem11  8375  phplem2  9199  epfrs  9710  zorng  10539  tsk2  10807  tskcard  10823  gruina  10860  muladd11  11437  00id  11442  ltaddneg  11483  negsub  11563  subneg  11564  muleqadd  11915  diveq0  11939  diveq1  11958  conjmul  11989  recp1lt1  12170  nnsub  12337  addltmul  12537  nnunb  12557  zltp1le  12701  gtndiv  12731  eluzp1m1  12946  zbtwnre  13028  rebtwnz  13029  xnn0le2is012  13331  supxrbnd  13413  divelunit  13580  fznatpl1  13666  flbi2  13911  fldiv  13954  modid  13990  modm1p1mod0  14019  fzen2  14066  nn0ennn  14076  seqshft2  14125  seqf1olem1  14138  ser1const  14155  sq01  14322  expnbnd  14329  faclbnd3  14389  faclbnd5  14395  hashunsng  14489  hashunsngx  14490  hashxplem  14531  ccatrid  14686  ccats1val1  14727  ccat2s1fst  14740  sgnn  15200  01sqrexlem2  15363  01sqrexlem7  15368  leabs  15419  abs2dif  15453  cvgrat  16005  cos2t  16299  sin01gt0  16311  cos01gt0  16312  demoivre  16321  demoivreALT  16322  rpnnen2lem5  16339  rpnnen2lem12  16346  omeo  16489  gcd0id  16642  sqgcd  16685  expgcd  16686  isprm3  16806  eulerthlem2  16906  pczpre  16972  pcrec  16983  ressress  17372  mulgm1  19251  unitgrpid  20562  mdet0pr  22854  m2detleib  22893  cmpcov2  23655  ufileu  24185  tgpconncompeqg  24378  itg2ge0  26003  mdegldg  26331  abssinper  26798  ppiub  27480  chtub  27488  bposlem2  27561  lgs1  27617  cofcutr  28229  addbday  28323  negbdaylem  28361  precsexlem10  28521  oncutlt  28569  n0bday  28657  bdayn0p1  28674  eucliddivs  28681  nnzs  28691  bdaypw2n0bndlem  28768  zz12s  28780  remulscllem1  28805  colinearalglem4  29406  axsegconlem1  29414  axpaschlem  29437  axcontlem2  29462  axcontlem4  29464  axcontlem7  29467  axcontlem8  29468  funvtxval  29515  funiedgval  29516  pthhashvtx  30234  vc0  31095  vcm  31097  nvmval2  31164  nvmf  31166  nvmdi  31169  nvnegneg  31170  nvpncan2  31174  nvaddsub4  31178  nvm1  31186  nvdif  31187  nvpi  31188  nvz0  31189  nvmtri  31192  nvabs  31193  nvge0  31194  imsmetlem  31211  4ipval2  31229  ipval3  31230  ipidsq  31231  dipcj  31235  sspmval  31254  ipasslem1  31352  ipasslem2  31353  dipsubdir  31369  hvsubdistr1  31570  shsubcl  31741  shsel3  31836  shunssi  31889  hosubdi  32329  lnopmi  32521  nmophmi  32552  nmopcoi  32616  opsqrlem6  32666  hstle  32751  hst0  32754  mdsl2i  32843  superpos  32875  dmdbr5ati  32943  f1rnen  33141  resvsca  33812  noinfepfnregs  35719  cvmliftphtlem  35997  mh-inf3f1  37245  topdifinffinlem  38184  finixpnum  38442  tan2h  38449  poimirlem3  38455  poimirlem4  38456  poimirlem7  38459  poimirlem16  38468  poimirlem17  38469  poimirlem19  38471  poimirlem20  38472  poimirlem24  38476  poimirlem28  38480  mblfinlem2  38490  mblfinlem4  38492  ismblfin  38493  el3v2  39077  atlatle  40291  pmaple  40732  dihglblem2N  42265  sn-ltaddneg  43440  elnnrabdioph  43746  rabren3dioph  43754  zindbi  43885  expgrowth  45257  binomcxplemnotnn0  45278  trelpss  45375  etransc  47209  mogoldbb  48799  pgrple2abl  49393  aacllem  50855