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

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

This theorem is referenced by:  mp3an12  1453  mp3an1i  1456  mp3anl1  1457  mp3an  1463  mp3an2i  1468  mp3an3an  1469  onint  7769  tfrlem9  8356  oaord1  8518  oaword2  8520  oawordeulem  8521  oa00  8526  omword1  8540  omword2  8541  omlimcl  8545  oeoelem  8565  nnaordex  8605  naddword1  8658  undom  9033  rexdif1enOLD  9129  sucdom2  9173  enp1iOLD  9232  fodomfi  9268  fodomfib  9287  dffi3  9389  unbnn3  9619  ttrcltr  9676  frmin  9709  frrlem16  9718  pwdjuen  10142  zorn2  10466  zornn0  10468  ttukey  10478  brdom7disj  10491  brdom6disj  10492  muladd11  11351  negsubdi  11485  mulneg1  11621  ltaddpos  11675  addge01  11695  reccl  11851  recid  11858  recid2  11859  div0  11877  recdiv2  11902  divdiv23zi  11942  ltmul12a  12045  lemul12a  12047  mulgt1OLD  12048  ltmulgt11  12049  gt0div  12056  ge0div  12057  lediv12a  12083  ledivp1  12092  ltdiv23i  12114  ledivp1i  12115  ltdivp1i  12116  infm3  12149  8th4div3  12409  gtndiv  12618  nn0ind  12636  xrre2  13137  2resupmax  13155  qsqueeze  13168  xmulpnf1  13241  xlemul1a  13255  ioorebas  13419  elfz0ubfz0  13600  le2sq2  14107  expubnd  14150  crreczi  14200  bccl  14294  hashbc  14425  wrdred1hash  14533  ccatlid  14558  shftfval  15043  sgnp  15063  sqreulem  15333  binom1p  15804  fallrisefac  15998  efsub  16075  efi4p  16112  sinadd  16139  cosadd  16140  demoivreALT  16176  rpnnen2lem4  16192  odd2np1  16318  opoe  16340  omoe  16341  opeo  16342  omeo  16343  divalglem4  16373  divalglem9  16378  gcdcllem3  16478  gcdadd  16503  algcvgblem  16554  isprm3  16660  1arith2  16906  vdwap0  16954  vdwap1  16955  ipolt  18501  smndex1sgrp  18842  f1otrspeq  19384  rmodislmod  20843  cnfldneg  21314  cnflddiv  21319  cnflddivOLD  21320  cnfldmulg  21322  cnfldexp  21323  zringsub  21372  zringmulg  21373  zringsubgval  21387  remulg  21523  resubgval  21525  thlleval  21614  mplsubrglem  21920  evls1rhm  22216  iccordt  23108  bl2ioo  24687  xrsblre  24707  iccntr  24717  icccmplem3  24720  reconnlem2  24723  opnreen  24727  mpomulcn  24765  iccpnfcnv  24849  cnllycmp  24862  pcoptcl  24928  ismbl2  25435  cmmbl  25442  nulmbl  25443  unmbl  25445  voliunlem2  25459  ioombl1  25470  opnmbllem  25509  mbfima  25538  ellimc3  25787  limcflf  25789  coe1termlem  26170  dvnply2  26202  dvnply  26203  reeff1o  26364  sinperlem  26396  resinf1o  26452  logeftb  26499  logge0  26521  efopn  26574  loglesqrt  26678  logrec  26680  xrlimcnp  26885  ppinncl  27091  chtrpcl  27092  bposlem2  27203  bposlem8  27209  lgsdir2  27248  1lgs  27258  nosupno  27622  nosupbday  27624  noinfno  27637  noinfbday  27639  noetasuplem4  27655  lrrecfr  27857  sltmul  28046  ax5seglem2  28863  axcontlem2  28899  fusgrfis  29264  3cyclfrgrrn  30222  isgrpoi  30434  imsmetlem  30626  nmcvcn  30631  ipval2  30643  lnocoi  30693  nmlno0lem  30729  nmblolbii  30735  blometi  30739  blocnilem  30740  blocni  30741  ipasslem1  30767  ipasslem2  30768  ipasslem4  30770  ipasslem5  30771  ipasslem8  30773  ipblnfi  30791  ip2eqi  30792  ubthlem1  30806  htthlem  30853  h2hmetdval  30914  axhvcom-zf  30919  axhis1-zf  30930  axhis4-zf  30933  hvm1neg  30968  hvsub4  30973  hvsubass  30980  hvsubdistr2  30986  hv2times  30997  hvsubcan  31010  hvsubcan2  31011  his2sub  31028  norm-i  31065  normpyc  31082  hhip  31113  hhph  31114  norm1exi  31186  hhssabloilem  31197  hhssnv  31200  hhshsslem2  31204  hhssmetdval  31213  shscli  31253  shunssi  31304  shsleji  31306  shsidmi  31320  spanunsni  31515  h1datomi  31517  spansncvi  31588  pjss2i  31616  pjssmii  31617  pjocini  31634  homullid  31736  honegdi  31745  ho2times  31755  nmopge0  31847  nmopgt0  31848  nmfnge0  31863  lnopaddi  31907  lnopmuli  31908  lnopsubi  31910  hmopbdoptHIL  31924  nmbdoplbi  31960  nmcoplbi  31964  nmophmi  31967  lnopconi  31970  lnfnaddi  31979  lnfnsubi  31982  nmbdfnlbi  31985  nmcfnlbi  31988  lnfnconi  31991  imaelshi  31994  cnlnadjlem2  32004  cnlnadjlem7  32009  nmoptrii  32030  nmopcoi  32031  adjcoi  32036  nmopcoadji  32037  bracnlnval  32050  leopmul  32070  opsqrlem1  32076  opsqrlem6  32081  hmopidmpji  32088  sto2i  32173  strlem1  32186  atcveq0  32284  atcv0eq  32315  atomli  32318  atcvati  32322  atcvat3i  32332  cdjreui  32368  cdj1i  32369  xdiv0  32856  xdivpnfrp  32860  mhmhmeotmd  33924  rezh  33966  qqhucn  33989  blsconn  35238  cnllysconn  35239  sate0fv0  35411  prv0  35424  sinccvglem  35666  opnrebl2  36316  ptrecube  37621  poimirlem6  37627  poimirlem7  37628  poimirlem29  37650  poimirlem30  37651  opnmbllem0  37657  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  voliunnfl  37665  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  heiborlem7  37818  rrnequiv  37836  ismrer1  37839  el3v1  38219  cnaddcom  38972  lcmineqlem1  42024  sn-ltaddpos  42448  mapco2  42710  mzpaddmpt  42736  mzpmulmpt  42737  zindbi  42942  mpaaeu  43146  tfsconcat0b  43342  eel000cT  44699  eel0TT  44700  supminfxr  45467  fmtno4prmfac  47577  pgn4cyclex  48120  aacllem  49794