Theorem mp3an1 1449

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 1121	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
4	1, 3	mpan 689	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  mp3an12  1452  mp3an1i  1455  mp3anl1  1456  mp3an  1462  mp3an2i  1467  mp3an3an  1468  onint  7775  wfrlem12OLD  8317  tfrlem9  8382  oaord1  8548  oaword2  8550  oawordeulem  8551  oa00  8556  omword1  8570  omword2  8571  omlimcl  8575  oeoelem  8595  nnaordex  8635  naddword1  8687  undom  9056  rexdif1enOLD  9156  sucdom2  9203  enp1iOLD  9277  dffi3  9423  unbnn3  9651  ttrcltr  9708  frmin  9741  frrlem16  9750  pwdjuen  10173  zorn2  10498  zornn0  10500  ttukey  10510  brdom7disj  10523  brdom6disj  10524  muladd11  11381  negsubdi  11513  mulneg1  11647  ltaddpos  11701  addge01  11721  reccl  11876  recid  11883  recid2  11884  recdiv2  11924  divdiv23zi  11964  ltmul12a  12067  lemul12a  12069  mulgt1  12070  ltmulgt11  12071  gt0div  12077  ge0div  12078  lediv12a  12104  ledivp1  12113  ltdiv23i  12135  ledivp1i  12136  ltdivp1i  12137  infm3  12170  8th4div3  12429  gtndiv  12636  nn0ind  12654  xrre2  13146  2resupmax  13164  qsqueeze  13177  xmulpnf1  13250  xlemul1a  13264  ioorebas  13425  elfz0ubfz0  13602  le2sq2  14097  expubnd  14139  crreczi  14188  bccl  14279  hashbc  14409  wrdred1hash  14508  ccatlid  14533  shftfval  15014  sgnp  15034  sqreulem  15303  binom1p  15774  fallrisefac  15966  efsub  16040  efi4p  16077  sinadd  16104  cosadd  16105  demoivreALT  16141  rpnnen2lem4  16157  odd2np1  16281  opoe  16303  omoe  16304  opeo  16305  omeo  16306  divalglem4  16336  divalglem9  16341  gcdcllem3  16439  gcdadd  16464  algcvgblem  16511  isprm3  16617  1arith2  16858  vdwap0  16906  vdwap1  16907  ipolt  18485  smndex1sgrp  18786  f1otrspeq  19310  rmodislmod  20533  rmodislmodOLD  20534  cnfldneg  20964  cnflddiv  20968  cnfldmulg  20970  cnfldexp  20971  zringmulg  21018  zringsubgval  21032  remulg  21152  resubgval  21154  thlleval  21245  mplsubrglem  21555  evls1rhm  21833  iccordt  22710  bl2ioo  24300  xrsblre  24319  iccntr  24329  icccmplem3  24332  reconnlem2  24335  opnreen  24339  iccpnfcnv  24452  cnllycmp  24464  pcoptcl  24529  ismbl2  25036  cmmbl  25043  nulmbl  25044  unmbl  25046  voliunlem2  25060  ioombl1  25071  opnmbllem  25110  mbfima  25139  ellimc3  25388  limcflf  25390  coe1termlem  25764  dvnply2  25792  dvnply  25793  reeff1o  25951  sinperlem  25982  resinf1o  26037  logeftb  26084  logge0  26105  efopn  26158  loglesqrt  26256  logrec  26258  xrlimcnp  26463  ppinncl  26668  chtrpcl  26669  bposlem2  26778  bposlem8  26784  lgsdir2  26823  1lgs  26833  nosupno  27196  nosupbday  27198  noinfno  27211  noinfbday  27213  noetasuplem4  27229  lrrecfr  27417  sltmul  27582  ax5seglem2  28177  axcontlem2  28213  fusgrfis  28577  3cyclfrgrrn  29529  isgrpoi  29739  imsmetlem  29931  nmcvcn  29936  ipval2  29948  lnocoi  29998  nmlno0lem  30034  nmblolbii  30040  blometi  30044  blocnilem  30045  blocni  30046  ipasslem1  30072  ipasslem2  30073  ipasslem4  30075  ipasslem5  30076  ipasslem8  30078  ipblnfi  30096  ip2eqi  30097  ubthlem1  30111  htthlem  30158  h2hmetdval  30219  axhvcom-zf  30224  axhis1-zf  30235  axhis4-zf  30238  hvm1neg  30273  hvsub4  30278  hvsubass  30285  hvsubdistr2  30291  hv2times  30302  hvsubcan  30315  hvsubcan2  30316  his2sub  30333  norm-i  30370  normpyc  30387  hhip  30418  hhph  30419  norm1exi  30491  hhssabloilem  30502  hhssnv  30505  hhshsslem2  30509  hhssmetdval  30518  shscli  30558  shunssi  30609  shsleji  30611  shsidmi  30625  spanunsni  30820  h1datomi  30822  spansncvi  30893  pjss2i  30921  pjssmii  30922  pjocini  30939  homullid  31041  honegdi  31050  ho2times  31060  nmopge0  31152  nmopgt0  31153  nmfnge0  31168  lnopaddi  31212  lnopmuli  31213  lnopsubi  31215  hmopbdoptHIL  31229  nmbdoplbi  31265  nmcoplbi  31269  nmophmi  31272  lnopconi  31275  lnfnaddi  31284  lnfnsubi  31287  nmbdfnlbi  31290  nmcfnlbi  31293  lnfnconi  31296  imaelshi  31299  cnlnadjlem2  31309  cnlnadjlem7  31314  nmoptrii  31335  nmopcoi  31336  adjcoi  31341  nmopcoadji  31342  bracnlnval  31355  leopmul  31375  opsqrlem1  31381  opsqrlem6  31386  hmopidmpji  31393  sto2i  31478  strlem1  31491  atcveq0  31589  atcv0eq  31620  atomli  31623  atcvati  31627  atcvat3i  31637  cdjreui  31673  cdj1i  31674  xdiv0  32083  xdivpnfrp  32087  mhmhmeotmd  32896  rezh  32940  qqhucn  32961  blsconn  34224  cnllysconn  34225  sate0fv0  34397  prv0  34410  sinccvglem  34646  opnrebl2  35195  ptrecube  36477  poimirlem6  36483  poimirlem7  36484  poimirlem29  36506  poimirlem30  36507  opnmbllem0  36513  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  voliunnfl  36521  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  heiborlem7  36674  rrnequiv  36692  ismrer1  36695  el3v1  37076  cnaddcom  37831  lcmineqlem1  40883  2xp3dxp2ge1d  41011  sn-ltaddpos  41311  mapco2  41439  mzpaddmpt  41465  mzpmulmpt  41466  zindbi  41671  mpaaeu  41878  tfsconcat0b  42082  eel000cT  43450  eel0TT  43451  supminfxr  44161  fmtno4prmfac  46227  aacllem  47802