Theorem mp3an1 1448

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 689	1 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  mp3an12  1451  mp3an1i  1454  mp3anl1  1455  mp3an  1461  mp3an2i  1466  mp3an3an  1467  onint  7826  wfrlem12OLD  8376  tfrlem9  8441  oaord1  8607  oaword2  8609  oawordeulem  8610  oa00  8615  omword1  8629  omword2  8630  omlimcl  8634  oeoelem  8654  nnaordex  8694  naddword1  8747  undom  9125  rexdif1enOLD  9225  sucdom2  9269  enp1iOLD  9342  fodomfi  9378  fodomfib  9397  dffi3  9500  unbnn3  9728  ttrcltr  9785  frmin  9818  frrlem16  9827  pwdjuen  10251  zorn2  10575  zornn0  10577  ttukey  10587  brdom7disj  10600  brdom6disj  10601  muladd11  11460  negsubdi  11592  mulneg1  11726  ltaddpos  11780  addge01  11800  reccl  11956  recid  11963  recid2  11964  div0  11982  recdiv2  12007  divdiv23zi  12047  ltmul12a  12150  lemul12a  12152  mulgt1OLD  12153  ltmulgt11  12154  gt0div  12161  ge0div  12162  lediv12a  12188  ledivp1  12197  ltdiv23i  12219  ledivp1i  12220  ltdivp1i  12221  infm3  12254  8th4div3  12513  gtndiv  12720  nn0ind  12738  xrre2  13232  2resupmax  13250  qsqueeze  13263  xmulpnf1  13336  xlemul1a  13350  ioorebas  13511  elfz0ubfz0  13689  le2sq2  14185  expubnd  14227  crreczi  14277  bccl  14371  hashbc  14502  wrdred1hash  14609  ccatlid  14634  shftfval  15119  sgnp  15139  sqreulem  15408  binom1p  15879  fallrisefac  16073  efsub  16148  efi4p  16185  sinadd  16212  cosadd  16213  demoivreALT  16249  rpnnen2lem4  16265  odd2np1  16389  opoe  16411  omoe  16412  opeo  16413  omeo  16414  divalglem4  16444  divalglem9  16449  gcdcllem3  16547  gcdadd  16572  algcvgblem  16624  isprm3  16730  1arith2  16975  vdwap0  17023  vdwap1  17024  ipolt  18605  smndex1sgrp  18943  f1otrspeq  19489  rmodislmod  20950  rmodislmodOLD  20951  cnfldneg  21431  cnflddiv  21436  cnflddivOLD  21437  cnfldmulg  21439  cnfldexp  21440  zringsub  21489  zringmulg  21490  zringsubgval  21504  remulg  21648  resubgval  21650  thlleval  21741  mplsubrglem  22047  evls1rhm  22347  iccordt  23243  bl2ioo  24833  xrsblre  24852  iccntr  24862  icccmplem3  24865  reconnlem2  24868  opnreen  24872  mpomulcn  24910  iccpnfcnv  24994  cnllycmp  25007  pcoptcl  25073  ismbl2  25581  cmmbl  25588  nulmbl  25589  unmbl  25591  voliunlem2  25605  ioombl1  25616  opnmbllem  25655  mbfima  25684  ellimc3  25934  limcflf  25936  coe1termlem  26317  dvnply2  26347  dvnply  26348  reeff1o  26509  sinperlem  26540  resinf1o  26596  logeftb  26643  logge0  26665  efopn  26718  loglesqrt  26822  logrec  26824  xrlimcnp  27029  ppinncl  27235  chtrpcl  27236  bposlem2  27347  bposlem8  27353  lgsdir2  27392  1lgs  27402  nosupno  27766  nosupbday  27768  noinfno  27781  noinfbday  27783  noetasuplem4  27799  lrrecfr  27994  sltmul  28180  ax5seglem2  28962  axcontlem2  28998  fusgrfis  29365  3cyclfrgrrn  30318  isgrpoi  30530  imsmetlem  30722  nmcvcn  30727  ipval2  30739  lnocoi  30789  nmlno0lem  30825  nmblolbii  30831  blometi  30835  blocnilem  30836  blocni  30837  ipasslem1  30863  ipasslem2  30864  ipasslem4  30866  ipasslem5  30867  ipasslem8  30869  ipblnfi  30887  ip2eqi  30888  ubthlem1  30902  htthlem  30949  h2hmetdval  31010  axhvcom-zf  31015  axhis1-zf  31026  axhis4-zf  31029  hvm1neg  31064  hvsub4  31069  hvsubass  31076  hvsubdistr2  31082  hv2times  31093  hvsubcan  31106  hvsubcan2  31107  his2sub  31124  norm-i  31161  normpyc  31178  hhip  31209  hhph  31210  norm1exi  31282  hhssabloilem  31293  hhssnv  31296  hhshsslem2  31300  hhssmetdval  31309  shscli  31349  shunssi  31400  shsleji  31402  shsidmi  31416  spanunsni  31611  h1datomi  31613  spansncvi  31684  pjss2i  31712  pjssmii  31713  pjocini  31730  homullid  31832  honegdi  31841  ho2times  31851  nmopge0  31943  nmopgt0  31944  nmfnge0  31959  lnopaddi  32003  lnopmuli  32004  lnopsubi  32006  hmopbdoptHIL  32020  nmbdoplbi  32056  nmcoplbi  32060  nmophmi  32063  lnopconi  32066  lnfnaddi  32075  lnfnsubi  32078  nmbdfnlbi  32081  nmcfnlbi  32084  lnfnconi  32087  imaelshi  32090  cnlnadjlem2  32100  cnlnadjlem7  32105  nmoptrii  32126  nmopcoi  32127  adjcoi  32132  nmopcoadji  32133  bracnlnval  32146  leopmul  32166  opsqrlem1  32172  opsqrlem6  32177  hmopidmpji  32184  sto2i  32269  strlem1  32282  atcveq0  32380  atcv0eq  32411  atomli  32414  atcvati  32418  atcvat3i  32428  cdjreui  32464  cdj1i  32465  xdiv0  32893  xdivpnfrp  32897  mhmhmeotmd  33873  rezh  33917  qqhucn  33938  blsconn  35212  cnllysconn  35213  sate0fv0  35385  prv0  35398  sinccvglem  35640  opnrebl2  36287  ptrecube  37580  poimirlem6  37586  poimirlem7  37587  poimirlem29  37609  poimirlem30  37610  opnmbllem0  37616  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  voliunnfl  37624  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  heiborlem7  37777  rrnequiv  37795  ismrer1  37798  el3v1  38178  cnaddcom  38928  lcmineqlem1  41986  2xp3dxp2ge1d  42198  sn-ltaddpos  42417  mapco2  42671  mzpaddmpt  42697  mzpmulmpt  42698  zindbi  42903  mpaaeu  43107  tfsconcat0b  43308  eel000cT  44674  eel0TT  44675  supminfxr  45379  fmtno4prmfac  47446  aacllem  48895