Theorem mp3an1 1447

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 1119	. 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  1450  mp3an1i  1453  mp3anl1  1454  mp3an  1460  mp3an2i  1465  mp3an3an  1466  onint  7809  wfrlem12OLD  8358  tfrlem9  8423  oaord1  8587  oaword2  8589  oawordeulem  8590  oa00  8595  omword1  8609  omword2  8610  omlimcl  8614  oeoelem  8634  nnaordex  8674  naddword1  8727  undom  9097  rexdif1enOLD  9197  sucdom2  9240  enp1iOLD  9311  fodomfi  9347  fodomfib  9366  dffi3  9468  unbnn3  9696  ttrcltr  9753  frmin  9786  frrlem16  9795  pwdjuen  10219  zorn2  10543  zornn0  10545  ttukey  10555  brdom7disj  10568  brdom6disj  10569  muladd11  11428  negsubdi  11562  mulneg1  11696  ltaddpos  11750  addge01  11770  reccl  11926  recid  11933  recid2  11934  div0  11952  recdiv2  11977  divdiv23zi  12017  ltmul12a  12120  lemul12a  12122  mulgt1OLD  12123  ltmulgt11  12124  gt0div  12131  ge0div  12132  lediv12a  12158  ledivp1  12167  ltdiv23i  12189  ledivp1i  12190  ltdivp1i  12191  infm3  12224  8th4div3  12483  gtndiv  12692  nn0ind  12710  xrre2  13208  2resupmax  13226  qsqueeze  13239  xmulpnf1  13312  xlemul1a  13326  ioorebas  13487  elfz0ubfz0  13668  le2sq2  14171  expubnd  14213  crreczi  14263  bccl  14357  hashbc  14488  wrdred1hash  14595  ccatlid  14620  shftfval  15105  sgnp  15125  sqreulem  15394  binom1p  15863  fallrisefac  16057  efsub  16132  efi4p  16169  sinadd  16196  cosadd  16197  demoivreALT  16233  rpnnen2lem4  16249  odd2np1  16374  opoe  16396  omoe  16397  opeo  16398  omeo  16399  divalglem4  16429  divalglem9  16434  gcdcllem3  16534  gcdadd  16559  algcvgblem  16610  isprm3  16716  1arith2  16961  vdwap0  17009  vdwap1  17010  ipolt  18592  smndex1sgrp  18933  f1otrspeq  19479  rmodislmod  20944  rmodislmodOLD  20945  cnfldneg  21425  cnflddiv  21430  cnflddivOLD  21431  cnfldmulg  21433  cnfldexp  21434  zringsub  21483  zringmulg  21484  zringsubgval  21498  remulg  21642  resubgval  21644  thlleval  21735  mplsubrglem  22041  evls1rhm  22341  iccordt  23237  bl2ioo  24827  xrsblre  24846  iccntr  24856  icccmplem3  24859  reconnlem2  24862  opnreen  24866  mpomulcn  24904  iccpnfcnv  24988  cnllycmp  25001  pcoptcl  25067  ismbl2  25575  cmmbl  25582  nulmbl  25583  unmbl  25585  voliunlem2  25599  ioombl1  25610  opnmbllem  25649  mbfima  25678  ellimc3  25928  limcflf  25930  coe1termlem  26311  dvnply2  26343  dvnply  26344  reeff1o  26505  sinperlem  26536  resinf1o  26592  logeftb  26639  logge0  26661  efopn  26714  loglesqrt  26818  logrec  26820  xrlimcnp  27025  ppinncl  27231  chtrpcl  27232  bposlem2  27343  bposlem8  27349  lgsdir2  27388  1lgs  27398  nosupno  27762  nosupbday  27764  noinfno  27777  noinfbday  27779  noetasuplem4  27795  lrrecfr  27990  sltmul  28176  ax5seglem2  28958  axcontlem2  28994  fusgrfis  29361  3cyclfrgrrn  30314  isgrpoi  30526  imsmetlem  30718  nmcvcn  30723  ipval2  30735  lnocoi  30785  nmlno0lem  30821  nmblolbii  30827  blometi  30831  blocnilem  30832  blocni  30833  ipasslem1  30859  ipasslem2  30860  ipasslem4  30862  ipasslem5  30863  ipasslem8  30865  ipblnfi  30883  ip2eqi  30884  ubthlem1  30898  htthlem  30945  h2hmetdval  31006  axhvcom-zf  31011  axhis1-zf  31022  axhis4-zf  31025  hvm1neg  31060  hvsub4  31065  hvsubass  31072  hvsubdistr2  31078  hv2times  31089  hvsubcan  31102  hvsubcan2  31103  his2sub  31120  norm-i  31157  normpyc  31174  hhip  31205  hhph  31206  norm1exi  31278  hhssabloilem  31289  hhssnv  31292  hhshsslem2  31296  hhssmetdval  31305  shscli  31345  shunssi  31396  shsleji  31398  shsidmi  31412  spanunsni  31607  h1datomi  31609  spansncvi  31680  pjss2i  31708  pjssmii  31709  pjocini  31726  homullid  31828  honegdi  31837  ho2times  31847  nmopge0  31939  nmopgt0  31940  nmfnge0  31955  lnopaddi  31999  lnopmuli  32000  lnopsubi  32002  hmopbdoptHIL  32016  nmbdoplbi  32052  nmcoplbi  32056  nmophmi  32059  lnopconi  32062  lnfnaddi  32071  lnfnsubi  32074  nmbdfnlbi  32077  nmcfnlbi  32080  lnfnconi  32083  imaelshi  32086  cnlnadjlem2  32096  cnlnadjlem7  32101  nmoptrii  32122  nmopcoi  32123  adjcoi  32128  nmopcoadji  32129  bracnlnval  32142  leopmul  32162  opsqrlem1  32168  opsqrlem6  32173  hmopidmpji  32180  sto2i  32265  strlem1  32278  atcveq0  32376  atcv0eq  32407  atomli  32410  atcvati  32414  atcvat3i  32424  cdjreui  32460  cdj1i  32461  xdiv0  32895  xdivpnfrp  32899  mhmhmeotmd  33887  rezh  33931  qqhucn  33954  blsconn  35228  cnllysconn  35229  sate0fv0  35401  prv0  35414  sinccvglem  35656  opnrebl2  36303  ptrecube  37606  poimirlem6  37612  poimirlem7  37613  poimirlem29  37635  poimirlem30  37636  opnmbllem0  37642  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  voliunnfl  37650  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  heiborlem7  37803  rrnequiv  37821  ismrer1  37824  el3v1  38204  cnaddcom  38953  lcmineqlem1  42010  2xp3dxp2ge1d  42222  sn-ltaddpos  42447  mapco2  42702  mzpaddmpt  42728  mzpmulmpt  42729  zindbi  42934  mpaaeu  43138  tfsconcat0b  43335  eel000cT  44700  eel0TT  44701  supminfxr  45413  fmtno4prmfac  47496  aacllem  49031