Theorem mpan9 506

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 34	. 2 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	impcom 407	1 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  sylan  581  vtocl2gf  3516  vtocl3gf  3517  vtocl2g  3518  vtocl3g  3519  sbcthdv  3745  elinsn  4655  axprlem4OLD  5367  swopolem  5542  wereu  5620  funssres  6536  dffv2  6929  fmptcof  7077  fnprb  7156  fntpb  7157  fliftfuns  7262  isorel  7274  oveqrspc2v  7387  caovclg  7552  caovcomg  7555  caovassg  7558  caovcang  7561  caovordig  7565  caovordg  7567  caovdig  7574  caovdirg  7577  caofidlcan  7662  peano5  7837  dmfexALT  7852  frpoins3xp3g  8084  fvmpocurryd  8214  qliftfuns  8744  nneneq  9133  ttrcltr  9628  ttrclselem2  9638  frins3  9670  cfslb  10179  hsmexlem4  10342  axdc3lem2  10364  axdc4lem  10368  adderpq  10870  mulerpq  10871  ltordlem  11666  lble  12099  uz11  12804  xrsupsslem  13250  xrinfmsslem  13251  xrsupss  13252  xrinfmss  13253  fseqsupubi  13931  hashbclem  14405  ccatass  14542  swrdswrd  14658  swrdccatin1  14678  swrdccatin2  14682  cshwcsh2id  14781  wwlktovf  14909  isercolllem1  15618  caucvgb  15633  zsum  15671  fsum  15673  fsumf1o  15676  fsumcvg2  15680  isummulc2  15715  fsum2dlem  15723  fsumcom2  15727  fsumshftm  15734  fsum0diag2  15736  fsum00  15752  fsumrlim  15765  o1fsum  15767  isumshft  15795  clim2prod  15844  ntrivcvgfvn0  15855  zprod  15893  fprod  15897  fprodf1o  15902  prodss  15903  fprodser  15905  fprodcllemf  15914  fprodm1s  15926  fprodp1s  15927  fprodabs  15930  fprod2dlem  15936  fprodcom2  15940  fprodefsum  16051  mod2eq1n2dvds  16307  sumeven  16347  lcmfun  16605  pythagtriplem4  16781  pcmptdvds  16856  prslem  18254  posi  18274  dlatmjdi  18480  lidrididd  18629  grpidinv2  18964  ghmlin  19187  cntzmhm2  19308  dprdss  19997  dprd2d2  20012  omndadd  20094  srgrz  20179  srglz  20180  ringinvnz1ne0  20272  rrgeq0i  20667  lmodlema  20851  islmodd  20852  lsscl  20928  lsslss  20947  lspdisjb  21116  lsslinds  21821  assalem  21847  fvmptnn04if  22824  chfacfscmulgsum  22835  chfacfpmmulgsum  22839  ssnei2  23091  t1ficld  23302  t1sep2  23344  unconn  23404  1stcclb  23419  ptbasfi  23556  tx1stc  23625  qtoptop2  23674  r0sep  23723  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  psmet0  24283  psmettri2  24284  prdsdsf  24342  prdsxmet  24344  cncfi  24871  ovolfiniun  25478  mbfimaopnlem  25632  limciun  25871  dvcn  25898  dvmptfsum  25952  dvfsumle  25998  dvfsumabs  26000  dvfsumlem3  26005  itgsubst  26026  fsumvma  27190  dchrelbasd  27216  dchrisumlem3  27468  ssslts1  27779  ssslts2  27780  madeval2  27839  elmade  27863  axcontlem9  29055  usgruspgrb  29266  uspgrloopvtxel  29600  umgr2v2evtxel  29606  clwwlknonex2lem2  30193  3spthd  30261  grpoass  30589  lnolin  30840  elnlfn  32014  strlem4  32340  hstrlem4  32348  atmd  32485  nn0min  32909  slmdlema  33279  qsxpid  33437  esumcvg  34246  measxun2  34370  sibfima  34498  bnj110  35016  bnj594  35070  bnj1491  35215  loop1cycl  35335  cvmcov  35461  mrsubcn  35717  dfon2lem5  35983  ifscgr  36242  nn0prpw  36521  neibastop2lem  36558  axnulregtco  36678  tr0el  36683  dfttc4  36728  bj-restb  37422  poimirlem25  37980  poimirlem32  37987  mbfresfi  38001  totbndss  38112  ghomlinOLD  38223  rngodi  38239  rngodir  38240  rngoass  38241  rngohomadd  38304  rngohommul  38305  crngocom  38336  idladdcl  38354  idllmulcl  38355  idlrmulcl  38356  exlimddvf  38456  oposlem  39642  cvlexch1  39788  hlsuprexch  39841  lautle  40544  elrfirn2  43142  wepwsolem  43488  kelac1  43509  islssfg2  43517  lnmlssfg  43526  onov0suclim  43720  relprel  45396  ovolval5lem3  47100  2elfz3nn0  47776  2elfz2melfz  47778  icceuelpartlem  47907  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  bgoldbtbnd  48297  gpgedg2iv  48555  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  oppcendc  49505  setrec2fun  50179