Theorem mp3an3 1580

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 1156	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
4	1, 3	mpi 20	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  mp3an13  1582  mp3an23  1583  mp3anl3  1587  opelxp  5379  ov  7041  ovmpt2a  7052  ovmpt2  7057  oaword1  7900  oneo  7929  oeoalem  7944  oeoelem  7946  nnaword1  7977  nnneo  7999  erov  8111  enrefg  8255  f1imaen  8285  mapxpen  8396  acnlem  9185  cdacomen  9319  infmap  9714  canthnumlem  9786  tskin  9897  tsksn  9898  tsk0  9901  gruxp  9945  gruina  9956  genpprecl  10139  addsrpr  10213  mulsrpr  10214  supsrlem  10249  mulid1  10355  00id  10531  mul02lem1  10532  ltneg  10853  leneg  10856  suble0  10867  div1  11042  nnaddcl  11375  nnmulcl  11376  nnmulclOLD  11377  nnge1  11381  nnsub  11396  2halves  11587  halfaddsub  11592  addltmul  11595  zleltp1  11757  nnaddm1cl  11763  zextlt  11780  eluzp1p1  11995  uzaddcl  12027  znq  12076  xrre  12289  xrre2  12290  fzshftral  12723  fraclt1  12899  expadd  13197  expmul  13200  expubnd  13216  sqmul  13221  bernneq  13285  faclbnd2  13372  faclbnd6  13380  hashgadd  13457  hashun2  13463  hashssdif  13490  hashfun  13514  ccatlcan  13808  ccatrcan  13809  pfx2  14069  shftval3  14194  sqrlem1  14361  caubnd2  14475  bpoly2  15161  bpoly3  15162  fsumcube  15164  efexp  15204  efival  15255  cos01gt0  15294  odd2np1  15440  halfleoddlt  15461  omoe  15463  opeo  15464  divalglem5  15495  gcdmultiple  15643  sqgcd  15652  nn0seqcvgd  15657  phiprmpw  15853  eulerthlem2  15859  odzcllem  15869  pythagtriplem15  15906  pythagtriplem17  15908  pcelnn  15946  4sqlem3  16026  xpscfn  16573  fullfunc  16919  fthfunc  16920  prfcl  17197  curf1cl  17222  curfcl  17226  hofcl  17253  odinv  18330  lsmelvalix  18408  dprdval  18757  lsp0  19369  lss0v  19376  coe1scl  20018  zndvds0  20259  frlmlbs  20504  lindfres  20530  lmisfree  20549  ntrin  21237  lpsscls  21317  restperf  21360  txuni2  21740  txopn  21777  elqtop2  21876  xkocnv  21989  ptcmp  22233  xblpnfps  22571  xblpnf  22572  bl2in  22576  unirnblps  22595  unirnbl  22596  blpnfctr  22612  dscopn  22749  bcthlem4  23496  minveclem2  23595  minveclem4  23601  icombl  23731  i1fadd  23862  i1fmul  23863  dvn1  24089  dvexp3  24141  plyconst  24362  plyid  24365  sincosq1eq  24665  sinord  24681  cxpp1  24826  cxpsqrtlem  24848  cxpsqrt  24849  angneg  24944  dcubic  24987  issqf  25276  ppiub  25343  bposlem1  25423  bposlem2  25424  bposlem9  25431  axlowdimlem6  26247  axlowdimlem14  26255  axcontlem2  26265  pthdlem2  27071  0ewlk  27491  ipasslem1  28242  ipasslem2  28243  ipasslem11  28251  minvecolem2  28287  minvecolem3  28288  minvecolem4  28292  shsva  28735  h1datomi  28996  lnfnmuli  29459  leopsq  29544  nmopleid  29554  opsqrlem6  29560  pjnmopi  29563  hstle  29645  csmdsymi  29749  atcvatlem  29800  dpfrac1  30146  elsx  30803  dya2iocnrect  30889  cvmliftphtlem  31846  wlimeq12  32304  frecseq123  32317  nosupno  32389  nosupfv  32392  scutval  32451  scutun12  32457  fvray  32788  fvline  32791  tailfb  32911  uncov  33934  tan2h  33945  matunitlindflem1  33950  matunitlindflem2  33951  poimirlem32  33986  mblfinlem4  33994  mbfresfi  34000  mbfposadd  34001  itg2addnc  34008  ftc1anclem5  34033  ftc1anclem8  34036  dvasin  34040  heiborlem7  34159  igenidl  34405  el3v3  34552  atlatmstc  35395  dihglblem2N  37370  eldioph4b  38220  diophren  38222  rmxp1  38341  rmyp1  38342  rmxm1  38343  rmym1  38344  wepwso  38457  dig0  43248  onetansqsecsq  43401  cotsqcscsq  43402