Theorem mp3an1 1450

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

Hypotheses

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

Assertion

Ref	Expression
mp3an1	⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem mp3an1

Step	Hyp	Ref	Expression
1		mp3an1.1	. 2 ⊢ 𝜑
2		mp3an1.2	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
3	2	3expb 1120	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 690	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mp3an12  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7747  tfrlem9  8331  oaord1  8493  oaword2  8495  oawordeulem  8496  oa00  8501  omword1  8515  omword2  8516  omlimcl  8520  oeoelem  8540  nnaordex  8580  naddword1  8633  undom  9007  rexdif1enOLD  9101  sucdom2  9145  enp1iOLD  9202  fodomfi  9238  fodomfib  9257  dffi3  9359  unbnn3  9591  ttrcltr  9648  frmin  9681  frrlem16  9690  pwdjuen  10114  zorn2  10438  zornn0  10440  ttukey  10450  brdom7disj  10463  brdom6disj  10464  muladd11  11323  negsubdi  11457  mulneg1  11593  ltaddpos  11647  addge01  11667  reccl  11823  recid  11830  recid2  11831  div0  11849  recdiv2  11874  divdiv23zi  11914  ltmul12a  12017  lemul12a  12019  mulgt1OLD  12020  ltmulgt11  12021  gt0div  12028  ge0div  12029  lediv12a  12055  ledivp1  12064  ltdiv23i  12086  ledivp1i  12087  ltdivp1i  12088  infm3  12121  8th4div3  12381  gtndiv  12590  nn0ind  12608  xrre2  13109  2resupmax  13127  qsqueeze  13140  xmulpnf1  13213  xlemul1a  13227  ioorebas  13391  elfz0ubfz0  13572  le2sq2  14079  expubnd  14122  crreczi  14172  bccl  14266  hashbc  14397  wrdred1hash  14505  ccatlid  14530  shftfval  15014  sgnp  15034  sqreulem  15304  binom1p  15775  fallrisefac  15969  efsub  16046  efi4p  16083  sinadd  16110  cosadd  16111  demoivreALT  16147  rpnnen2lem4  16163  odd2np1  16289  opoe  16311  omoe  16312  opeo  16313  omeo  16314  divalglem4  16344  divalglem9  16349  gcdcllem3  16449  gcdadd  16474  algcvgblem  16525  isprm3  16631  1arith2  16877  vdwap0  16925  vdwap1  16926  ipolt  18478  smndex1sgrp  18819  f1otrspeq  19363  rmodislmod  20870  cnfldneg  21339  cnflddiv  21344  cnflddivOLD  21345  cnfldmulg  21347  cnfldexp  21348  zringsub  21399  zringmulg  21400  zringsubgval  21414  remulg  21551  resubgval  21553  thlleval  21642  mplsubrglem  21948  evls1rhm  22244  iccordt  23136  bl2ioo  24715  xrsblre  24735  iccntr  24745  icccmplem3  24748  reconnlem2  24751  opnreen  24755  mpomulcn  24793  iccpnfcnv  24877  cnllycmp  24890  pcoptcl  24956  ismbl2  25463  cmmbl  25470  nulmbl  25471  unmbl  25473  voliunlem2  25487  ioombl1  25498  opnmbllem  25537  mbfima  25566  ellimc3  25815  limcflf  25817  coe1termlem  26198  dvnply2  26230  dvnply  26231  reeff1o  26392  sinperlem  26424  resinf1o  26480  logeftb  26527  logge0  26549  efopn  26602  loglesqrt  26706  logrec  26708  xrlimcnp  26913  ppinncl  27119  chtrpcl  27120  bposlem2  27231  bposlem8  27237  lgsdir2  27276  1lgs  27286  nosupno  27650  nosupbday  27652  noinfno  27665  noinfbday  27667  noetasuplem4  27683  lrrecfr  27892  sltmul  28081  ax5seglem2  28911  axcontlem2  28947  fusgrfis  29312  3cyclfrgrrn  30267  isgrpoi  30479  imsmetlem  30671  nmcvcn  30676  ipval2  30688  lnocoi  30738  nmlno0lem  30774  nmblolbii  30780  blometi  30784  blocnilem  30785  blocni  30786  ipasslem1  30812  ipasslem2  30813  ipasslem4  30815  ipasslem5  30816  ipasslem8  30818  ipblnfi  30836  ip2eqi  30837  ubthlem1  30851  htthlem  30898  h2hmetdval  30959  axhvcom-zf  30964  axhis1-zf  30975  axhis4-zf  30978  hvm1neg  31013  hvsub4  31018  hvsubass  31025  hvsubdistr2  31031  hv2times  31042  hvsubcan  31055  hvsubcan2  31056  his2sub  31073  norm-i  31110  normpyc  31127  hhip  31158  hhph  31159  norm1exi  31231  hhssabloilem  31242  hhssnv  31245  hhshsslem2  31249  hhssmetdval  31258  shscli  31298  shunssi  31349  shsleji  31351  shsidmi  31365  spanunsni  31560  h1datomi  31562  spansncvi  31633  pjss2i  31661  pjssmii  31662  pjocini  31679  homullid  31781  honegdi  31790  ho2times  31800  nmopge0  31892  nmopgt0  31893  nmfnge0  31908  lnopaddi  31952  lnopmuli  31953  lnopsubi  31955  hmopbdoptHIL  31969  nmbdoplbi  32005  nmcoplbi  32009  nmophmi  32012  lnopconi  32015  lnfnaddi  32024  lnfnsubi  32027  nmbdfnlbi  32030  nmcfnlbi  32033  lnfnconi  32036  imaelshi  32039  cnlnadjlem2  32049  cnlnadjlem7  32054  nmoptrii  32075  nmopcoi  32076  adjcoi  32081  nmopcoadji  32082  bracnlnval  32095  leopmul  32115  opsqrlem1  32121  opsqrlem6  32126  hmopidmpji  32133  sto2i  32218  strlem1  32231  atcveq0  32329  atcv0eq  32360  atomli  32363  atcvati  32367  atcvat3i  32377  cdjreui  32413  cdj1i  32414  xdiv0  32901  xdivpnfrp  32905  mhmhmeotmd  33912  rezh  33954  qqhucn  33977  blsconn  35226  cnllysconn  35227  sate0fv0  35399  prv0  35412  sinccvglem  35654  opnrebl2  36304  ptrecube  37609  poimirlem6  37615  poimirlem7  37616  poimirlem29  37638  poimirlem30  37639  opnmbllem0  37645  mblfinlem3  37648  mblfinlem4  37649  ismblfin  37650  voliunnfl  37653  ftc1anclem5  37686  ftc1anclem7  37688  ftc1anclem8  37689  ftc1anc  37690  heiborlem7  37806  rrnequiv  37824  ismrer1  37827  el3v1  38207  cnaddcom  38960  lcmineqlem1  42012  sn-ltaddpos  42436  mapco2  42698  mzpaddmpt  42724  mzpmulmpt  42725  zindbi  42930  mpaaeu  43134  tfsconcat0b  43330  eel000cT  44687  eel0TT  44688  supminfxr  45455  fmtno4prmfac  47568  pgn4cyclex  48111  aacllem  49785