Theorem mp3an1 1444

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 395  df-3an 1086

This theorem is referenced by:  mp3an12  1447  mp3an1i  1450  mp3anl1  1451  mp3an  1457  mp3an2i  1462  mp3an3an  1463  onint  7799  wfrlem12OLD  8347  tfrlem9  8412  oaord1  8578  oaword2  8580  oawordeulem  8581  oa00  8586  omword1  8600  omword2  8601  omlimcl  8605  oeoelem  8625  nnaordex  8665  naddword1  8718  undom  9090  rexdif1enOLD  9190  sucdom2  9237  enp1iOLD  9311  dffi3  9462  unbnn3  9690  ttrcltr  9747  frmin  9780  frrlem16  9789  pwdjuen  10212  zorn2  10537  zornn0  10539  ttukey  10549  brdom7disj  10562  brdom6disj  10563  muladd11  11422  negsubdi  11554  mulneg1  11688  ltaddpos  11742  addge01  11762  reccl  11917  recid  11924  recid2  11925  recdiv2  11965  divdiv23zi  12005  ltmul12a  12108  lemul12a  12110  mulgt1  12111  ltmulgt11  12112  gt0div  12118  ge0div  12119  lediv12a  12145  ledivp1  12154  ltdiv23i  12176  ledivp1i  12177  ltdivp1i  12178  infm3  12211  8th4div3  12470  gtndiv  12677  nn0ind  12695  xrre2  13189  2resupmax  13207  qsqueeze  13220  xmulpnf1  13293  xlemul1a  13307  ioorebas  13468  elfz0ubfz0  13645  le2sq2  14139  expubnd  14181  crreczi  14230  bccl  14321  hashbc  14452  wrdred1hash  14551  ccatlid  14576  shftfval  15057  sgnp  15077  sqreulem  15346  binom1p  15817  fallrisefac  16009  efsub  16084  efi4p  16121  sinadd  16148  cosadd  16149  demoivreALT  16185  rpnnen2lem4  16201  odd2np1  16325  opoe  16347  omoe  16348  opeo  16349  omeo  16350  divalglem4  16380  divalglem9  16385  gcdcllem3  16483  gcdadd  16508  algcvgblem  16555  isprm3  16661  1arith2  16904  vdwap0  16952  vdwap1  16953  ipolt  18534  smndex1sgrp  18867  f1otrspeq  19409  rmodislmod  20820  rmodislmodOLD  20821  cnfldneg  21330  cnflddiv  21335  cnflddivOLD  21336  cnfldmulg  21338  cnfldexp  21339  zringsub  21388  zringmulg  21389  zringsubgval  21403  remulg  21546  resubgval  21548  thlleval  21639  mplsubrglem  21953  evls1rhm  22248  iccordt  23138  bl2ioo  24728  xrsblre  24747  iccntr  24757  icccmplem3  24760  reconnlem2  24763  opnreen  24767  mpomulcn  24805  iccpnfcnv  24889  cnllycmp  24902  pcoptcl  24968  ismbl2  25476  cmmbl  25483  nulmbl  25484  unmbl  25486  voliunlem2  25500  ioombl1  25511  opnmbllem  25550  mbfima  25579  ellimc3  25828  limcflf  25830  coe1termlem  26212  dvnply2  26242  dvnply  26243  reeff1o  26404  sinperlem  26435  resinf1o  26490  logeftb  26537  logge0  26559  efopn  26612  loglesqrt  26713  logrec  26715  xrlimcnp  26920  ppinncl  27126  chtrpcl  27127  bposlem2  27238  bposlem8  27244  lgsdir2  27283  1lgs  27293  nosupno  27656  nosupbday  27658  noinfno  27671  noinfbday  27673  noetasuplem4  27689  lrrecfr  27880  sltmul  28056  ax5seglem2  28760  axcontlem2  28796  fusgrfis  29163  3cyclfrgrrn  30116  isgrpoi  30328  imsmetlem  30520  nmcvcn  30525  ipval2  30537  lnocoi  30587  nmlno0lem  30623  nmblolbii  30629  blometi  30633  blocnilem  30634  blocni  30635  ipasslem1  30661  ipasslem2  30662  ipasslem4  30664  ipasslem5  30665  ipasslem8  30667  ipblnfi  30685  ip2eqi  30686  ubthlem1  30700  htthlem  30747  h2hmetdval  30808  axhvcom-zf  30813  axhis1-zf  30824  axhis4-zf  30827  hvm1neg  30862  hvsub4  30867  hvsubass  30874  hvsubdistr2  30880  hv2times  30891  hvsubcan  30904  hvsubcan2  30905  his2sub  30922  norm-i  30959  normpyc  30976  hhip  31007  hhph  31008  norm1exi  31080  hhssabloilem  31091  hhssnv  31094  hhshsslem2  31098  hhssmetdval  31107  shscli  31147  shunssi  31198  shsleji  31200  shsidmi  31214  spanunsni  31409  h1datomi  31411  spansncvi  31482  pjss2i  31510  pjssmii  31511  pjocini  31528  homullid  31630  honegdi  31639  ho2times  31649  nmopge0  31741  nmopgt0  31742  nmfnge0  31757  lnopaddi  31801  lnopmuli  31802  lnopsubi  31804  hmopbdoptHIL  31818  nmbdoplbi  31854  nmcoplbi  31858  nmophmi  31861  lnopconi  31864  lnfnaddi  31873  lnfnsubi  31876  nmbdfnlbi  31879  nmcfnlbi  31882  lnfnconi  31885  imaelshi  31888  cnlnadjlem2  31898  cnlnadjlem7  31903  nmoptrii  31924  nmopcoi  31925  adjcoi  31930  nmopcoadji  31931  bracnlnval  31944  leopmul  31964  opsqrlem1  31970  opsqrlem6  31975  hmopidmpji  31982  sto2i  32067  strlem1  32080  atcveq0  32178  atcv0eq  32209  atomli  32212  atcvati  32216  atcvat3i  32226  cdjreui  32262  cdj1i  32263  xdiv0  32673  xdivpnfrp  32677  mhmhmeotmd  33561  rezh  33605  qqhucn  33626  blsconn  34887  cnllysconn  34888  sate0fv0  35060  prv0  35073  sinccvglem  35309  opnrebl2  35838  ptrecube  37126  poimirlem6  37132  poimirlem7  37133  poimirlem29  37155  poimirlem30  37156  opnmbllem0  37162  mblfinlem3  37165  mblfinlem4  37166  ismblfin  37167  voliunnfl  37170  ftc1anclem5  37203  ftc1anclem7  37205  ftc1anclem8  37206  ftc1anc  37207  heiborlem7  37323  rrnequiv  37341  ismrer1  37344  el3v1  37725  cnaddcom  38476  lcmineqlem1  41532  2xp3dxp2ge1d  41725  sn-ltaddpos  42027  mapco2  42166  mzpaddmpt  42192  mzpmulmpt  42193  zindbi  42398  mpaaeu  42605  tfsconcat0b  42806  eel000cT  44173  eel0TT  44174  supminfxr  44875  fmtno4prmfac  46941  aacllem  48312