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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  mp3an12  1450  mp3an1i  1453  mp3anl1  1454  mp3an  1460  mp3an2i  1465  mp3an3an  1466  onint  7634  wfrlem12OLD  8142  tfrlem9  8207  oaord1  8367  oaword2  8369  oawordeulem  8370  oa00  8375  omword1  8389  omword2  8390  omlimcl  8394  oeoelem  8414  nnaordex  8454  rexdif1en  8926  enp1i  9030  dffi3  9168  unbnn3  9395  ttrcltr  9452  frmin  9507  pwdjuen  9938  zorn2  10263  zornn0  10265  ttukey  10275  brdom7disj  10288  brdom6disj  10289  muladd11  11145  negsubdi  11277  mulneg1  11411  ltaddpos  11465  addge01  11485  reccl  11640  recid  11647  recid2  11648  recdiv2  11688  divdiv23zi  11728  ltmul12a  11831  lemul12a  11833  mulgt1  11834  ltmulgt11  11835  gt0div  11841  ge0div  11842  lediv12a  11868  ledivp1  11877  ltdiv23i  11899  ledivp1i  11900  ltdivp1i  11901  infm3  11934  8th4div3  12193  gtndiv  12397  nn0ind  12415  xrre2  12903  2resupmax  12921  qsqueeze  12934  xmulpnf1  13007  xlemul1a  13021  ioorebas  13182  elfz0ubfz0  13359  le2sq2  13852  expubnd  13893  crreczi  13941  bccl  14034  hashbc  14163  wrdred1hash  14262  ccatlid  14289  shftfval  14779  sgnp  14799  sqreulem  15069  binom1p  15541  fallrisefac  15733  efsub  15807  efi4p  15844  sinadd  15871  cosadd  15872  demoivreALT  15908  rpnnen2lem4  15924  odd2np1  16048  opoe  16070  omoe  16071  opeo  16072  omeo  16073  divalglem4  16103  divalglem9  16108  gcdcllem3  16206  gcdadd  16231  algcvgblem  16280  isprm3  16386  1arith2  16627  vdwap0  16675  vdwap1  16676  ipolt  18251  smndex1sgrp  18545  f1otrspeq  19053  rmodislmod  20189  rmodislmodOLD  20190  cnfldneg  20622  cnflddiv  20626  cnfldmulg  20628  cnfldexp  20629  zringmulg  20676  zringsubgval  20690  remulg  20810  resubgval  20812  thlleval  20903  mplsubrglem  21208  evls1rhm  21486  iccordt  22363  bl2ioo  23953  xrsblre  23972  iccntr  23982  icccmplem3  23985  reconnlem2  23988  opnreen  23992  iccpnfcnv  24105  cnllycmp  24117  pcoptcl  24182  ismbl2  24689  cmmbl  24696  nulmbl  24697  unmbl  24699  voliunlem2  24713  ioombl1  24724  opnmbllem  24763  mbfima  24792  ellimc3  25041  limcflf  25043  coe1termlem  25417  dvnply2  25445  dvnply  25446  reeff1o  25604  sinperlem  25635  resinf1o  25690  logeftb  25737  logge0  25758  efopn  25811  loglesqrt  25909  logrec  25911  xrlimcnp  26116  ppinncl  26321  chtrpcl  26322  bposlem2  26431  bposlem8  26437  lgsdir2  26476  1lgs  26486  ax5seglem2  27295  axcontlem2  27331  fusgrfis  27695  3cyclfrgrrn  28646  isgrpoi  28856  imsmetlem  29048  nmcvcn  29053  ipval2  29065  lnocoi  29115  nmlno0lem  29151  nmblolbii  29157  blometi  29161  blocnilem  29162  blocni  29163  ipasslem1  29189  ipasslem2  29190  ipasslem4  29192  ipasslem5  29193  ipasslem8  29195  ipblnfi  29213  ip2eqi  29214  ubthlem1  29228  htthlem  29275  h2hmetdval  29336  axhvcom-zf  29341  axhis1-zf  29352  axhis4-zf  29355  hvm1neg  29390  hvsub4  29395  hvsubass  29402  hvsubdistr2  29408  hv2times  29419  hvsubcan  29432  hvsubcan2  29433  his2sub  29450  norm-i  29487  normpyc  29504  hhip  29535  hhph  29536  norm1exi  29608  hhssabloilem  29619  hhssnv  29622  hhshsslem2  29626  hhssmetdval  29635  shscli  29675  shunssi  29726  shsleji  29728  shsidmi  29742  spanunsni  29937  h1datomi  29939  spansncvi  30010  pjss2i  30038  pjssmii  30039  pjocini  30056  homulid2  30158  honegdi  30167  ho2times  30177  nmopge0  30269  nmopgt0  30270  nmfnge0  30285  lnopaddi  30329  lnopmuli  30330  lnopsubi  30332  hmopbdoptHIL  30346  nmbdoplbi  30382  nmcoplbi  30386  nmophmi  30389  lnopconi  30392  lnfnaddi  30401  lnfnsubi  30404  nmbdfnlbi  30407  nmcfnlbi  30410  lnfnconi  30413  imaelshi  30416  cnlnadjlem2  30426  cnlnadjlem7  30431  nmoptrii  30452  nmopcoi  30453  adjcoi  30458  nmopcoadji  30459  bracnlnval  30472  leopmul  30492  opsqrlem1  30498  opsqrlem6  30503  hmopidmpji  30510  sto2i  30595  strlem1  30608  atcveq0  30706  atcv0eq  30737  atomli  30740  atcvati  30744  atcvat3i  30754  cdjreui  30790  cdj1i  30791  xdiv0  31199  xdivpnfrp  31203  mhmhmeotmd  31873  rezh  31917  qqhucn  31938  blsconn  33202  cnllysconn  33203  sate0fv0  33375  prv0  33388  sinccvglem  33626  nosupno  33902  nosupbday  33904  noinfno  33917  noinfbday  33919  noetasuplem4  33935  lrrecfr  34096  opnrebl2  34506  ptrecube  35773  poimirlem6  35779  poimirlem7  35780  poimirlem29  35802  poimirlem30  35803  opnmbllem0  35809  mblfinlem3  35812  mblfinlem4  35813  ismblfin  35814  voliunnfl  35817  ftc1anclem5  35850  ftc1anclem7  35852  ftc1anclem8  35853  ftc1anc  35854  heiborlem7  35971  rrnequiv  35989  ismrer1  35992  el3v1  36368  cnaddcom  36982  lcmineqlem1  40034  2xp3dxp2ge1d  40159  sn-ltaddpos  40420  mapco2  40534  mzpaddmpt  40560  mzpmulmpt  40561  zindbi  40765  mpaaeu  40972  eel000cT  42293  eel0TT  42294  supminfxr  42975  fmtno4prmfac  44993  aacllem  46474