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  7746  tfrlem9  8330  oaord1  8492  oaword2  8494  oawordeulem  8495  oa00  8500  omword1  8514  omword2  8515  omlimcl  8519  oeoelem  8539  nnaordex  8579  naddword1  8632  undom  9006  rexdif1enOLD  9100  sucdom2  9144  enp1iOLD  9201  fodomfi  9237  fodomfib  9256  dffi3  9358  unbnn3  9590  ttrcltr  9647  frmin  9680  frrlem16  9689  pwdjuen  10113  zorn2  10437  zornn0  10439  ttukey  10449  brdom7disj  10462  brdom6disj  10463  muladd11  11322  negsubdi  11456  mulneg1  11592  ltaddpos  11646  addge01  11666  reccl  11822  recid  11829  recid2  11830  div0  11848  recdiv2  11873  divdiv23zi  11913  ltmul12a  12016  lemul12a  12018  mulgt1OLD  12019  ltmulgt11  12020  gt0div  12027  ge0div  12028  lediv12a  12054  ledivp1  12063  ltdiv23i  12085  ledivp1i  12086  ltdivp1i  12087  infm3  12120  8th4div3  12380  gtndiv  12589  nn0ind  12607  xrre2  13108  2resupmax  13126  qsqueeze  13139  xmulpnf1  13212  xlemul1a  13226  ioorebas  13390  elfz0ubfz0  13571  le2sq2  14078  expubnd  14121  crreczi  14171  bccl  14265  hashbc  14396  wrdred1hash  14504  ccatlid  14529  shftfval  15013  sgnp  15033  sqreulem  15303  binom1p  15774  fallrisefac  15968  efsub  16045  efi4p  16082  sinadd  16109  cosadd  16110  demoivreALT  16146  rpnnen2lem4  16162  odd2np1  16288  opoe  16310  omoe  16311  opeo  16312  omeo  16313  divalglem4  16343  divalglem9  16348  gcdcllem3  16448  gcdadd  16473  algcvgblem  16524  isprm3  16630  1arith2  16876  vdwap0  16924  vdwap1  16925  ipolt  18477  smndex1sgrp  18818  f1otrspeq  19362  rmodislmod  20869  cnfldneg  21338  cnflddiv  21343  cnflddivOLD  21344  cnfldmulg  21346  cnfldexp  21347  zringsub  21398  zringmulg  21399  zringsubgval  21413  remulg  21550  resubgval  21552  thlleval  21641  mplsubrglem  21947  evls1rhm  22243  iccordt  23135  bl2ioo  24714  xrsblre  24734  iccntr  24744  icccmplem3  24747  reconnlem2  24750  opnreen  24754  mpomulcn  24792  iccpnfcnv  24876  cnllycmp  24889  pcoptcl  24955  ismbl2  25462  cmmbl  25469  nulmbl  25470  unmbl  25472  voliunlem2  25486  ioombl1  25497  opnmbllem  25536  mbfima  25565  ellimc3  25814  limcflf  25816  coe1termlem  26197  dvnply2  26229  dvnply  26230  reeff1o  26391  sinperlem  26423  resinf1o  26479  logeftb  26526  logge0  26548  efopn  26601  loglesqrt  26705  logrec  26707  xrlimcnp  26912  ppinncl  27118  chtrpcl  27119  bposlem2  27230  bposlem8  27236  lgsdir2  27275  1lgs  27285  nosupno  27649  nosupbday  27651  noinfno  27664  noinfbday  27666  noetasuplem4  27682  lrrecfr  27891  sltmul  28080  ax5seglem2  28910  axcontlem2  28946  fusgrfis  29311  3cyclfrgrrn  30266  isgrpoi  30478  imsmetlem  30670  nmcvcn  30675  ipval2  30687  lnocoi  30737  nmlno0lem  30773  nmblolbii  30779  blometi  30783  blocnilem  30784  blocni  30785  ipasslem1  30811  ipasslem2  30812  ipasslem4  30814  ipasslem5  30815  ipasslem8  30817  ipblnfi  30835  ip2eqi  30836  ubthlem1  30850  htthlem  30897  h2hmetdval  30958  axhvcom-zf  30963  axhis1-zf  30974  axhis4-zf  30977  hvm1neg  31012  hvsub4  31017  hvsubass  31024  hvsubdistr2  31030  hv2times  31041  hvsubcan  31054  hvsubcan2  31055  his2sub  31072  norm-i  31109  normpyc  31126  hhip  31157  hhph  31158  norm1exi  31230  hhssabloilem  31241  hhssnv  31244  hhshsslem2  31248  hhssmetdval  31257  shscli  31297  shunssi  31348  shsleji  31350  shsidmi  31364  spanunsni  31559  h1datomi  31561  spansncvi  31632  pjss2i  31660  pjssmii  31661  pjocini  31678  homullid  31780  honegdi  31789  ho2times  31799  nmopge0  31891  nmopgt0  31892  nmfnge0  31907  lnopaddi  31951  lnopmuli  31952  lnopsubi  31954  hmopbdoptHIL  31968  nmbdoplbi  32004  nmcoplbi  32008  nmophmi  32011  lnopconi  32014  lnfnaddi  32023  lnfnsubi  32026  nmbdfnlbi  32029  nmcfnlbi  32032  lnfnconi  32035  imaelshi  32038  cnlnadjlem2  32048  cnlnadjlem7  32053  nmoptrii  32074  nmopcoi  32075  adjcoi  32080  nmopcoadji  32081  bracnlnval  32094  leopmul  32114  opsqrlem1  32120  opsqrlem6  32125  hmopidmpji  32132  sto2i  32217  strlem1  32230  atcveq0  32328  atcv0eq  32359  atomli  32362  atcvati  32366  atcvat3i  32376  cdjreui  32412  cdj1i  32413  xdiv0  32900  xdivpnfrp  32904  mhmhmeotmd  33911  rezh  33953  qqhucn  33976  blsconn  35225  cnllysconn  35226  sate0fv0  35398  prv0  35411  sinccvglem  35653  opnrebl2  36303  ptrecube  37608  poimirlem6  37614  poimirlem7  37615  poimirlem29  37637  poimirlem30  37638  opnmbllem0  37644  mblfinlem3  37647  mblfinlem4  37648  ismblfin  37649  voliunnfl  37652  ftc1anclem5  37685  ftc1anclem7  37687  ftc1anclem8  37688  ftc1anc  37689  heiborlem7  37805  rrnequiv  37823  ismrer1  37826  el3v1  38206  cnaddcom  38959  lcmineqlem1  42011  sn-ltaddpos  42435  mapco2  42697  mzpaddmpt  42723  mzpmulmpt  42724  zindbi  42929  mpaaeu  43133  tfsconcat0b  43329  eel000cT  44686  eel0TT  44687  supminfxr  45454  fmtno4prmfac  47567  pgn4cyclex  48110  aacllem  49784