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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  mp3an12  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7574  wfrlem12  8066  tfrlem9  8121  oaord1  8279  oaword2  8281  oawordeulem  8282  oa00  8287  omword1  8301  omword2  8302  omlimcl  8306  oeoelem  8326  nnaordex  8366  rexdif1en  8839  enp1i  8909  dffi3  9047  unbnn3  9274  pwdjuen  9795  zorn2  10120  zornn0  10122  ttukey  10132  brdom7disj  10145  brdom6disj  10146  muladd11  11002  negsubdi  11134  mulneg1  11268  ltaddpos  11322  addge01  11342  reccl  11497  recid  11504  recid2  11505  recdiv2  11545  divdiv23zi  11585  ltmul12a  11688  lemul12a  11690  mulgt1  11691  ltmulgt11  11692  gt0div  11698  ge0div  11699  lediv12a  11725  ledivp1  11734  ltdiv23i  11756  ledivp1i  11757  ltdivp1i  11758  infm3  11791  8th4div3  12050  gtndiv  12254  nn0ind  12272  xrre2  12760  2resupmax  12778  qsqueeze  12791  xmulpnf1  12864  xlemul1a  12878  ioorebas  13039  elfz0ubfz0  13216  le2sq2  13706  expubnd  13747  crreczi  13795  bccl  13888  hashbc  14017  wrdred1hash  14116  ccatlid  14143  shftfval  14633  sgnp  14653  sqreulem  14923  binom1p  15395  fallrisefac  15587  efsub  15661  efi4p  15698  sinadd  15725  cosadd  15726  demoivreALT  15762  rpnnen2lem4  15778  odd2np1  15902  opoe  15924  omoe  15925  opeo  15926  omeo  15927  divalglem4  15957  divalglem9  15962  gcdcllem3  16060  gcdadd  16085  algcvgblem  16134  isprm3  16240  1arith2  16481  vdwap0  16529  vdwap1  16530  ipolt  18041  smndex1sgrp  18335  f1otrspeq  18839  rmodislmod  19967  cnfldneg  20389  cnflddiv  20393  cnfldmulg  20395  cnfldexp  20396  zringmulg  20443  zringsubgval  20457  remulg  20569  resubgval  20571  thlleval  20660  mplsubrglem  20966  evls1rhm  21238  iccordt  22111  bl2ioo  23689  xrsblre  23708  iccntr  23718  icccmplem3  23721  reconnlem2  23724  opnreen  23728  iccpnfcnv  23841  cnllycmp  23853  pcoptcl  23918  ismbl2  24424  cmmbl  24431  nulmbl  24432  unmbl  24434  voliunlem2  24448  ioombl1  24459  opnmbllem  24498  mbfima  24527  ellimc3  24776  limcflf  24778  coe1termlem  25152  dvnply2  25180  dvnply  25181  reeff1o  25339  sinperlem  25370  resinf1o  25425  logeftb  25472  logge0  25493  efopn  25546  loglesqrt  25644  logrec  25646  xrlimcnp  25851  ppinncl  26056  chtrpcl  26057  bposlem2  26166  bposlem8  26172  lgsdir2  26211  1lgs  26221  ax5seglem2  27020  axcontlem2  27056  fusgrfis  27418  3cyclfrgrrn  28369  isgrpoi  28579  imsmetlem  28771  nmcvcn  28776  ipval2  28788  lnocoi  28838  nmlno0lem  28874  nmblolbii  28880  blometi  28884  blocnilem  28885  blocni  28886  ipasslem1  28912  ipasslem2  28913  ipasslem4  28915  ipasslem5  28916  ipasslem8  28918  ipblnfi  28936  ip2eqi  28937  ubthlem1  28951  htthlem  28998  h2hmetdval  29059  axhvcom-zf  29064  axhis1-zf  29075  axhis4-zf  29078  hvm1neg  29113  hvsub4  29118  hvsubass  29125  hvsubdistr2  29131  hv2times  29142  hvsubcan  29155  hvsubcan2  29156  his2sub  29173  norm-i  29210  normpyc  29227  hhip  29258  hhph  29259  norm1exi  29331  hhssabloilem  29342  hhssnv  29345  hhshsslem2  29349  hhssmetdval  29358  shscli  29398  shunssi  29449  shsleji  29451  shsidmi  29465  spanunsni  29660  h1datomi  29662  spansncvi  29733  pjss2i  29761  pjssmii  29762  pjocini  29779  homulid2  29881  honegdi  29890  ho2times  29900  nmopge0  29992  nmopgt0  29993  nmfnge0  30008  lnopaddi  30052  lnopmuli  30053  lnopsubi  30055  hmopbdoptHIL  30069  nmbdoplbi  30105  nmcoplbi  30109  nmophmi  30112  lnopconi  30115  lnfnaddi  30124  lnfnsubi  30127  nmbdfnlbi  30130  nmcfnlbi  30133  lnfnconi  30136  imaelshi  30139  cnlnadjlem2  30149  cnlnadjlem7  30154  nmoptrii  30175  nmopcoi  30176  adjcoi  30181  nmopcoadji  30182  bracnlnval  30195  leopmul  30215  opsqrlem1  30221  opsqrlem6  30226  hmopidmpji  30233  sto2i  30318  strlem1  30331  atcveq0  30429  atcv0eq  30460  atomli  30463  atcvati  30467  atcvat3i  30477  cdjreui  30513  cdj1i  30514  xdiv0  30923  xdivpnfrp  30927  mhmhmeotmd  31591  rezh  31633  qqhucn  31654  blsconn  32919  cnllysconn  32920  sate0fv0  33092  prv0  33105  sinccvglem  33343  ttrcltr  33515  nosupno  33643  nosupbday  33645  noinfno  33658  noinfbday  33660  noetasuplem4  33676  lrrecfr  33837  opnrebl2  34247  ptrecube  35514  poimirlem6  35520  poimirlem7  35521  poimirlem29  35543  poimirlem30  35544  opnmbllem0  35550  mblfinlem3  35553  mblfinlem4  35554  ismblfin  35555  voliunnfl  35558  ftc1anclem5  35591  ftc1anclem7  35593  ftc1anclem8  35594  ftc1anc  35595  heiborlem7  35712  rrnequiv  35730  ismrer1  35733  el3v1  36109  cnaddcom  36723  lcmineqlem1  39771  2xp3dxp2ge1d  39884  sn-ltaddpos  40131  mapco2  40240  mzpaddmpt  40266  mzpmulmpt  40267  zindbi  40471  mpaaeu  40678  eel000cT  41996  eel0TT  41997  supminfxr  42679  fmtno4prmfac  44697  aacllem  46176