Theorem mp3an1 1457

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

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

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  mp3an12  1460  mp3an1i  1463  mp3anl1  1464  mp3an  1470  mp3an2i  1475  mp3an3an  1476  onint  7737  tfrlem9  8318  oaord1  8480  oaword2  8482  oawordeulem  8483  oa00  8488  omword1  8502  omword2  8503  omlimcl  8507  oeoelem  8528  nnaordex  8568  naddword1  8621  undom  8997  sucdom2  9131  fodomfi  9216  fodomfib  9233  dffi3  9338  unbnn3  9575  ttrcltr  9632  frmin  9668  frrlem16  9677  pwdjuen  10099  zorn2  10423  zornn0  10425  ttukey  10435  brdom7disj  10448  brdom6disj  10449  muladd11  11311  negsubdi  11445  mulneg1  11581  ltaddpos  11635  addge01  11655  reccl  11811  recid  11818  recid2  11819  div0  11837  recdiv2  11863  divdiv23zi  11903  ltmul12a  12006  lemul12a  12008  mulgt1OLD  12009  ltmulgt11  12010  gt0div  12017  ge0div  12018  lediv12a  12044  ledivp1  12053  ltdiv23i  12075  ledivp1i  12076  ltdivp1i  12077  infm3  12110  8th4div3  12392  gtndiv  12601  nn0ind  12619  xrre2  13117  2resupmax  13135  qsqueeze  13148  xmulpnf1  13221  xlemul1a  13235  ioorebas  13399  elfz0ubfz0  13581  le2sq2  14092  expubnd  14135  crreczi  14185  bccl  14279  hashbc  14410  wrdred1hash  14518  ccatlid  14544  shftfval  15027  sgnp  15047  sqreulem  15317  binom1p  15791  fallrisefac  15985  efsub  16062  efi4p  16099  sinadd  16126  cosadd  16127  demoivreALT  16163  rpnnen2lem4  16179  odd2np1  16305  opoe  16327  omoe  16328  opeo  16329  omeo  16330  divalglem4  16360  divalglem9  16365  gcdcllem3  16465  gcdadd  16490  algcvgblem  16541  isprm3  16647  1arith2  16894  vdwap0  16942  vdwap1  16943  ipolt  18496  smndex1sgrp  18874  f1otrspeq  19417  rmodislmod  20924  cnfldneg  21377  cnflddiv  21381  cnfldmulg  21383  cnfldexp  21384  zringsub  21434  zringmulg  21435  zringsubgval  21449  remulg  21586  resubgval  21588  thlleval  21677  mplsubrglem  21982  evls1rhm  22312  iccordt  23201  bl2ioo  24779  xrsblre  24799  iccntr  24809  icccmplem3  24812  reconnlem2  24815  opnreen  24819  mpomulcn  24856  iccpnfcnv  24933  cnllycmp  24945  pcoptcl  25010  ismbl2  25516  cmmbl  25523  nulmbl  25524  unmbl  25526  voliunlem2  25540  ioombl1  25551  opnmbllem  25590  mbfima  25619  ellimc3  25868  limcflf  25870  coe1termlem  26245  dvnply2  26275  dvnply  26276  reeff1o  26434  sinperlem  26466  resinf1o  26522  logeftb  26569  logge0  26591  efopn  26644  loglesqrt  26747  logrec  26749  xrlimcnp  26954  ppinncl  27159  chtrpcl  27160  bposlem2  27270  bposlem8  27276  lgsdir2  27315  1lgs  27325  nosupno  27689  nosupbday  27691  noinfno  27704  noinfbday  27706  noetasuplem4  27722  lrrecfr  27957  ltmuls  28150  bdayfinbndlem1  28481  ax5seglem2  29020  axcontlem2  29056  fusgrfis  29421  3cyclfrgrrn  30378  isgrpoi  30591  imsmetlem  30783  nmcvcn  30788  ipval2  30800  lnocoi  30850  nmlno0lem  30886  nmblolbii  30892  blometi  30896  blocnilem  30897  blocni  30898  ipasslem1  30924  ipasslem2  30925  ipasslem4  30927  ipasslem5  30928  ipasslem8  30930  ipblnfi  30948  ip2eqi  30949  ubthlem1  30963  htthlem  31010  h2hmetdval  31071  axhvcom-zf  31076  axhis1-zf  31087  axhis4-zf  31090  hvm1neg  31125  hvsub4  31130  hvsubass  31137  hvsubdistr2  31143  hv2times  31154  hvsubcan  31167  hvsubcan2  31168  his2sub  31185  norm-i  31222  normpyc  31239  hhip  31270  hhph  31271  norm1exi  31343  hhssabloilem  31354  hhssnv  31357  hhshsslem2  31361  hhssmetdval  31370  shscli  31410  shunssi  31461  shsleji  31463  shsidmi  31477  spanunsni  31672  h1datomi  31674  spansncvi  31745  pjss2i  31773  pjssmii  31774  pjocini  31791  homullid  31893  honegdi  31902  ho2times  31912  nmopge0  32004  nmopgt0  32005  nmfnge0  32020  lnopaddi  32064  lnopmuli  32065  lnopsubi  32067  hmopbdoptHIL  32081  nmbdoplbi  32117  nmcoplbi  32121  nmophmi  32124  lnopconi  32127  lnfnaddi  32136  lnfnsubi  32139  nmbdfnlbi  32142  nmcfnlbi  32145  lnfnconi  32148  imaelshi  32151  cnlnadjlem2  32161  cnlnadjlem7  32166  nmoptrii  32187  nmopcoi  32188  adjcoi  32193  nmopcoadji  32194  bracnlnval  32207  leopmul  32227  opsqrlem1  32233  opsqrlem6  32238  hmopidmpji  32245  sto2i  32330  strlem1  32343  atcveq0  32441  atcv0eq  32472  atomli  32475  atcvati  32479  atcvat3i  32489  cdjreui  32525  cdj1i  32526  xdiv0  33011  xdivpnfrp  33015  mhmhmeotmd  34123  rezh  34165  qqhucn  34188  blsconn  35487  cnllysconn  35488  sate0fv0  35660  prv0  35673  sinccvglem  35915  opnrebl2  36564  ptrecube  38002  poimirlem6  38008  poimirlem7  38009  poimirlem29  38031  poimirlem30  38032  opnmbllem0  38038  mblfinlem3  38041  mblfinlem4  38042  ismblfin  38043  voliunnfl  38046  ftc1anclem5  38079  ftc1anclem7  38081  ftc1anclem8  38082  ftc1anc  38083  heiborlem7  38199  rrnequiv  38217  ismrer1  38220  el3v1  38612  preuniqval  38878  cnaddcom  39479  lcmineqlem1  42529  sn-ltaddpos  42958  mapco2  43179  mzpaddmpt  43205  mzpmulmpt  43206  zindbi  43406  mpaaeu  43610  tfsconcat0b  43806  eel000cT  45161  eel0TT  45162  supminfxr  45921  fmtno4prmfac  48064  pgn4cyclex  48631  aacllem  50305