Theorem mp3an3 1479

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 1139	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 21	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:  mp3an13  1481  mp3an23  1482  mp3anl3  1486  el3v3  3462  opelxp  5695  ov  7560  ovmpoa  7571  ovmpo  7576  frecseq123  8284  oaword1  8542  oneo  8571  oeoalem  8587  oeoelem  8589  nnaword1  8620  nnneo  8646  erov  8817  uncov  8875  enrefg  8993  f1imaen  9026  mapxpen  9144  0sdom1dom  9219  acnlem  10054  djucomen  10183  nnadju  10203  infmap  10588  canthnumlem  10660  tskin  10771  tsksn  10772  tsk0  10775  gruxp  10819  gruina  10830  genpprecl  11013  addsrpr  11087  mulsrpr  11088  supsrlem  11123  mulrid  11233  00id  11412  mul02lem1  11413  ltneg  11741  leneg  11744  suble0  11755  div1  11931  nnaddcl  12283  nnmulcl  12284  nnge1  12291  nnsub  12307  2halves  12489  halfaddsub  12504  addltmul  12507  fcdmnn0fsuppg  12591  zleltp1  12672  nnaddm1cl  12681  zextlt  12698  eluzp1p1  12918  uzaddcl  12956  znq  13004  xrre  13223  xrre2  13224  fzshftral  13672  fraclt1  13865  expadd  14170  expmul  14173  sqmul  14185  expubnd  14244  bernneq  14295  faclbnd2  14357  faclbnd6  14365  hashgadd  14443  hashun2  14449  hashunsnggt  14460  hashssdif  14479  hashfun  14504  ccatlcan  14789  ccatrcan  14790  pfx2  15020  shftval3  15151  01sqrexlem1  15331  caubnd2  15447  bpoly2  16147  bpoly3  16148  fsumcube  16150  efexp  16193  efival  16244  cos01gt0  16283  odd2np1  16435  halfleoddlt  16456  omoe  16458  opeo  16459  divalglem5  16491  sqgcd  16656  nn0seqcvgd  16664  prmdvdssq  16813  phiprmpw  16871  eulerthlem2  16877  odzcllem  16888  pythagtriplem15  16925  pythagtriplem17  16927  pcelnn  16966  4sqlem3  17046  fullfunc  18001  fthfunc  18002  prfcl  18295  curf1cl  18320  curfcl  18324  hofcl  18351  odinv  19689  lsmelvalix  19769  dprdval  20133  lsp0  21194  lss0v  21201  zndvds0  21764  frlmlbs  22011  lindfres  22037  lmisfree  22056  coe1scl  22514  matunitlindflem1  22902  matunitlindflem2  22903  ntrin  23287  lpsscls  23367  restperf  23410  txuni2  23792  txopn  23829  elqtop2  23928  xkocnv  24041  ptcmp  24285  xblpnfps  24622  xblpnf  24623  bl2in  24627  unirnblps  24646  unirnbl  24647  blpnfctr  24663  dscopn  24800  bcthlem4  25556  minveclem2  25655  minveclem4  25661  icombl  25793  i1fadd  25924  i1fmul  25925  dvn1  26155  dvexp3  26207  plyconst  26433  plyid  26436  sincosq1eq  26747  sinord  26769  cxpp1  26915  cxpsqrtlem  26937  cxpsqrt  26938  angneg  27038  dcubic  27081  issqf  27370  ppiub  27438  bposlem1  27518  bposlem2  27519  bposlem9  27526  nosupno  27937  nosupfv  27940  noinfno  27952  noinffv  27955  cutsval  28043  cutsun12  28053  cuteq0  28078  cuteq1  28080  cofcut1  28183  cofcutr  28187  addcuts2  28242  leadds1  28252  addsuniflem  28264  addsasslem1  28266  addsasslem2  28267  negcut2  28303  mulsproplem12  28390  mulcut2  28396  divs1  28467  precsexlem10  28479  precsexlem11  28480  bdayons  28539  n0s0suc  28605  nnzsubs  28648  zmulscld  28660  elz12si  28736  axlowdimlem6  29390  axlowdimlem14  29398  axcontlem2  29408  pthdlem2  30219  0ewlk  30570  ipasslem1  31298  ipasslem2  31299  ipasslem11  31307  minvecolem2  31342  minvecolem3  31343  minvecolem4  31347  shsva  31787  h1datomi  32048  lnfnmuli  32511  leopsq  32596  nmopleid  32606  opsqrlem6  32612  pjnmopi  32615  hstle  32697  csmdsymi  32801  atcvatlem  32852  dpfrac1  33324  cshf1o  33389  rspidlid  33796  elsx  34692  dya2iocnrect  34779  r1omhf  35601  cvmliftphtlem  35883  satfv1  35929  satffunlem1lem2  35969  satffunlem1  35973  wlimeq12  36383  fvray  36708  fvline  36711  tailfb  36983  ttc0elw  37133  tan2h  38353  poimirlem32  38388  mblfinlem4  38396  mbfresfi  38402  mbfposadd  38403  itg2addnc  38410  ftc1anclem5  38433  ftc1anclem8  38436  dvasin  38440  heiborlem7  38554  igenidl  38800  atlatmstc  40179  dihglblem2N  42154  eldioph4b  43639  diophren  43641  rmxp1  43760  rmyp1  43761  rmxm1  43762  rmym1  43763  dfgric2  48818  gpgov  48945  dig0  49523  i0oii  49833  iinfconstbas  49979  onetansqsecsq  50674  cotsqcscsq  50675