Theorem mp3an3 1478

Description: An inference based on modus ponens. (Contributed by NM, 21-Nov-1994.)

Hypotheses

Ref	Expression
mp3an3.1	⊢ 𝜒
mp3an3.2	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an3	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem mp3an3

Step	Hyp	Ref	Expression
1		mp3an3.1	. 2 ⊢ 𝜒
2		mp3an3.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expia 1138	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 21	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

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 401  df-3an 1104

This theorem is used by:  mp3an13  1480  mp3an23  1481  mp3anl3  1485  el3v3  3463  opelxp  5696  ov  7556  ovmpoa  7567  ovmpo  7572  frecseq123  8277  oaword1  8535  oneo  8564  oeoalem  8580  oeoelem  8582  nnaword1  8613  nnneo  8639  erov  8810  enrefg  8979  f1imaen  9012  mapxpen  9129  0sdom1dom  9204  acnlem  10039  djucomen  10168  nnadju  10188  infmap  10567  canthnumlem  10639  tskin  10750  tsksn  10751  tsk0  10754  gruxp  10798  gruina  10809  genpprecl  10992  addsrpr  11066  mulsrpr  11067  supsrlem  11102  mulrid  11212  00id  11391  mul02lem1  11392  ltneg  11720  leneg  11723  suble0  11734  div1  11910  nnaddcl  12262  nnmulcl  12263  nnge1  12270  nnsub  12286  2halves  12468  halfaddsub  12483  addltmul  12486  fcdmnn0fsuppg  12570  zleltp1  12651  nnaddm1cl  12659  zextlt  12676  eluzp1p1  12896  uzaddcl  12934  znq  12982  xrre  13201  xrre2  13202  fzshftral  13650  fraclt1  13842  expadd  14147  expmul  14150  sqmul  14162  expubnd  14221  bernneq  14272  faclbnd2  14334  faclbnd6  14342  hashgadd  14420  hashun2  14426  hashunsnggt  14437  hashssdif  14456  hashfun  14481  ccatlcan  14762  ccatrcan  14763  pfx2  14991  shftval3  15120  01sqrexlem1  15300  caubnd2  15416  bpoly2  16117  bpoly3  16118  fsumcube  16120  efexp  16163  efival  16214  cos01gt0  16253  odd2np1  16405  halfleoddlt  16426  omoe  16428  opeo  16429  divalglem5  16461  sqgcd  16626  nn0seqcvgd  16634  prmdvdssq  16783  phiprmpw  16841  eulerthlem2  16847  odzcllem  16858  pythagtriplem15  16895  pythagtriplem17  16897  pcelnn  16936  4sqlem3  17016  fullfunc  17971  fthfunc  17972  prfcl  18265  curf1cl  18290  curfcl  18294  hofcl  18321  odinv  19637  lsmelvalix  19717  dprdval  20081  lsp0  21141  lss0v  21148  zndvds0  21711  frlmlbs  21958  lindfres  21984  lmisfree  22003  coe1scl  22459  ntrin  23229  lpsscls  23309  restperf  23352  txuni2  23733  txopn  23770  elqtop2  23869  xkocnv  23982  ptcmp  24226  xblpnfps  24563  xblpnf  24564  bl2in  24568  unirnblps  24587  unirnbl  24588  blpnfctr  24604  dscopn  24741  bcthlem4  25497  minveclem2  25596  minveclem4  25602  icombl  25734  i1fadd  25865  i1fmul  25866  dvn1  26096  dvexp3  26148  plyconst  26374  plyid  26377  sincosq1eq  26688  sinord  26710  cxpp1  26856  cxpsqrtlem  26878  cxpsqrt  26879  angneg  26979  dcubic  27022  issqf  27311  ppiub  27379  bposlem1  27459  bposlem2  27460  bposlem9  27467  nosupno  27878  nosupfv  27881  noinfno  27893  noinffv  27896  cutsval  27984  cutsun12  27994  cuteq0  28019  cuteq1  28021  cofcut1  28124  cofcutr  28128  addcuts2  28183  leadds1  28193  addsuniflem  28205  addsasslem1  28207  addsasslem2  28208  negcut2  28244  mulsproplem12  28331  mulcut2  28337  divs1  28408  precsexlem10  28420  precsexlem11  28421  bdayons  28480  n0s0suc  28546  nnzsubs  28589  zmulscld  28601  elz12si  28677  axlowdimlem6  29308  axlowdimlem14  29316  axcontlem2  29326  pthdlem2  30128  0ewlk  30476  ipasslem1  31194  ipasslem2  31195  ipasslem11  31203  minvecolem2  31238  minvecolem3  31239  minvecolem4  31243  shsva  31683  h1datomi  31944  lnfnmuli  32407  leopsq  32492  nmopleid  32502  opsqrlem6  32508  pjnmopi  32511  hstle  32593  csmdsymi  32697  atcvatlem  32748  dpfrac1  33222  cshf1o  33291  rspidlid  33698  elsx  34593  dya2iocnrect  34680  r1omhf  35509  cvmliftphtlem  35817  satfv1  35863  satffunlem1lem2  35903  satffunlem1  35907  wlimeq12  36317  fvray  36641  fvline  36644  tailfb  36916  ttc0elw  37066  uncov  38280  tan2h  38291  matunitlindflem1  38295  matunitlindflem2  38296  poimirlem32  38331  mblfinlem4  38339  mbfresfi  38345  mbfposadd  38346  itg2addnc  38353  ftc1anclem5  38376  ftc1anclem8  38379  dvasin  38383  heiborlem7  38496  igenidl  38742  atlatmstc  40121  dihglblem2N  42096  eldioph4b  43566  diophren  43568  rmxp1  43687  rmyp1  43688  rmxm1  43689  rmym1  43690  dfgric2  48708  gpgov  48835  dig0  49414  i0oii  49726  iinfconstbas  49872  onetansqsecsq  50567  cotsqcscsq  50568