Theorem mpan9 516

Description: Modus ponens conjoining dissimilar antecedents. (Contributed by NM, 1-Feb-2008.) (Proof shortened by Andrew Salmon, 7-May-2011.)

Hypotheses

Ref	Expression
mpan9.1	⊢ (𝜑 → 𝜓)
mpan9.2	⊢ (𝜒 → (𝜓 → 𝜃))

Assertion

Ref	Expression
mpan9	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Proof of Theorem mpan9

Step	Hyp	Ref	Expression
1		mpan9.1	. . 3 ⊢ (𝜑 → 𝜓)
2		mpan9.2	. . 3 ⊢ (𝜒 → (𝜓 → 𝜃))
3	1, 2	syl5 35	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 413	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  sylan  592  vtocl2gf  3531  vtocl3gf  3532  vtocl2g  3533  vtocl3g  3534  sbcthdv  3754  elinsn  4667  swopolem  5568  wereu  5646  funssres  6585  dffv2  6981  fmptcof  7132  fnprb  7215  fntpb  7216  fliftfuns  7323  isorel  7335  oveqrspc2v  7448  caovclg  7614  caovcomg  7617  caovassg  7620  caovcang  7623  caovordig  7627  caovordg  7629  caovdig  7636  caovdirg  7639  caofidlcan  7732  peano5  7906  dmfexALT  7921  frpoins3xp3g  8161  fvmpocurryd  8292  qliftfuns  8829  nneneq  9225  ttrcltr  9721  ttrclselem2  9731  frins3  9763  setrec2fun  9977  cfslb  10348  hsmexlem4  10511  axdc3lem2  10533  axdc4lem  10537  adderpq  11045  mulerpq  11046  ltordlem  11845  lble  12273  uz11  12994  xrsupsslem  13441  xrinfmsslem  13442  xrsupss  13443  xrinfmss  13444  fseqsupubi  14125  hashbclem  14601  ccatass  14738  swrdswrd  14859  swrdccatin1  14879  swrdccatin2  14883  cshwcsh2id  14984  wwlktovf  15115  isercolllem1  15838  caucvgb  15853  zsum  15890  fsum  15892  fsumf1o  15895  fsumcvg2  15899  isummulc2  15934  fsum2dlem  15942  fsumcom2  15946  fsumshftm  15953  fsum0diag2  15955  fsum00  15971  fsumrlim  15984  o1fsum  15986  isumshft  16014  clim2prod  16063  ntrivcvgfvn0  16074  zprod  16110  fprod  16114  fprodf1o  16119  prodss  16120  fprodser  16122  fprodcllemf  16131  fprodm1s  16143  fprodp1s  16144  fprodabs  16147  fprod2dlem  16153  fprodcom2  16157  fprodefsum  16267  mod2eq1n2dvds  16523  sumeven  16563  sumodd  16564  lcmfun  16826  pythagtriplem4  17003  pcmptdvds  17078  prslem  18477  posi  18497  dlatmjdi  18703  lidrididd  18857  grpidinv2  19214  qsxpid  19393  ghmlin  19441  cntzmhm2  19562  dprdss  20251  dprd2d2  20266  omndadd  20348  srgrz  20439  srglz  20440  ringinvnz1ne0  20537  rrgeq0i  20957  lmodlema  21146  islmodd  21147  lsscl  21223  lsslss  21242  lspdisjb  21410  lsslinds  22143  assalem  22171  fvmptnn04if  23173  chfacfscmulgsum  23184  chfacfpmmulgsum  23188  ssnei2  23440  t1ficld  23651  t1sep2  23693  unconn  23753  1stcclb  23768  ptbasfi  23906  tx1stc  23975  qtoptop2  24024  r0sep  24073  ustincl  24533  ustdiag  24534  ustinvel  24535  ustexhalf  24536  psmet0  24633  psmettri2  24634  prdsdsf  24692  prdsxmet  24694  cncfi  25221  ovolfiniun  25828  mbfimaopnlem  25982  limciun  26220  dvcn  26247  dvmptfsum  26301  dvfsumle  26347  dvfsumabs  26349  dvfsumlem3  26354  itgsubst  26375  fsumvma  27546  dchrelbasd  27572  dchrisumlem3  27824  ssslts1  28165  ssslts2  28166  madeval2  28225  elmade  28249  axcontlem9  29556  usgruspgrb  29770  uspgrloopvtxel  30103  umgr2v2evtxel  30109  clwwlknonex2lem2  30705  loop1cycl  30750  3spthd  30783  grpoass  31111  lnolin  31362  elnlfn  32536  strlem4  32862  hstrlem4  32870  atmd  33007  nn0min  33459  slmdlema  33811  esumcvg  34765  measxun2  34890  sibfima  35017  bnj110  35535  bnj594  35589  bnj1491  35734  dfac16  35811  acwer1prc  35817  cvmcov  36115  mrsubcn  36371  dfon2lem5  36642  ifscgr  36902  nn0prpw  37204  neibastop2lem  37241  axnulregtco  37361  tr0el  37366  dfttc4  37411  bj-restb  38108  poimirlem25  38657  poimirlem32  38664  mbfresfi  38678  totbndss  38805  ghomlinOLD  38916  rngodi  38932  rngodir  38933  rngoass  38934  rngohomadd  38997  rngohommul  38998  crngocom  39029  idladdcl  39047  idllmulcl  39048  idlrmulcl  39049  exlimddvf  39147  oposlem  40333  cvlexch1  40479  hlsuprexch  40532  lautle  41235  elrfirn2  43801  wepwsolem  44143  kelac1  44159  islssfg2  44167  lnmlssfg  44176  onov0suclim  44370  relprel  46035  ovolval5lem3  47758  2elfz3nn0  48480  2elfz2melfz  48482  icceuelpartlem  48611  wtgoldbnnsum4prm  48994  bgoldbnnsum3prm  48996  bgoldbtbnd  49001  gpgedg2iv  49259  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem6  49316  oppcendc  50226