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  580  vtocl2gf  3555  vtocl3gf  3556  vtocl2g  3557  vtocl3g  3558  vtoclegftOLD  3572  sbcthdv  3786  elinsn  4690  axprlem4OLD  5409  swopolem  5582  wereu  5661  funssres  6590  dffv2  6984  fmptcof  7130  fnprb  7210  fntpb  7211  fliftfuns  7316  isorel  7328  oveqrspc2v  7440  caovclg  7607  caovcomg  7610  caovassg  7613  caovcang  7616  caovordig  7620  caovordg  7622  caovdig  7629  caovdirg  7632  caofidlcan  7717  peano5  7897  dmfexALT  7912  frpoins3xp3g  8148  fvmpocurryd  8278  qliftfuns  8826  nneneq  9228  nneneqOLD  9240  ttrcltr  9738  ttrclselem2  9748  frins3  9777  cfslb  10288  hsmexlem4  10451  axdc3lem2  10473  axdc4lem  10477  adderpq  10978  mulerpq  10979  ltordlem  11770  lble  12202  uz11  12885  xrsupsslem  13331  xrinfmsslem  13332  xrsupss  13333  xrinfmss  13334  fseqsupubi  14001  hashbclem  14474  ccatass  14609  swrdswrd  14726  swrdccatin1  14746  swrdccatin2  14750  cshwcsh2id  14850  wwlktovf  14978  isercolllem1  15684  caucvgb  15699  zsum  15737  fsum  15739  fsumf1o  15742  fsumcvg2  15746  isummulc2  15781  fsum2dlem  15789  fsumcom2  15793  fsumshftm  15800  fsum0diag2  15802  fsum00  15817  fsumrlim  15830  o1fsum  15832  isumshft  15858  clim2prod  15907  ntrivcvgfvn0  15918  zprod  15956  fprod  15960  fprodf1o  15965  prodss  15966  fprodser  15968  fprodcllemf  15977  fprodm1s  15989  fprodp1s  15990  fprodabs  15993  fprod2dlem  15999  fprodcom2  16003  fprodefsum  16114  mod2eq1n2dvds  16367  sumeven  16407  lcmfun  16665  pythagtriplem4  16840  pcmptdvds  16915  prslem  18314  posi  18334  dlatmjdi  18538  lidrididd  18653  grpidinv2  18985  ghmlin  19209  cntzmhm2  19330  dprdss  20018  dprd2d2  20033  srgrz  20173  srglz  20174  ringinvnz1ne0  20266  rrgeq0i  20668  lmodlema  20832  islmodd  20833  lsscl  20909  lsslss  20928  lspdisjb  21097  lsslinds  21806  assalem  21832  fvmptnn04if  22804  chfacfscmulgsum  22815  chfacfpmmulgsum  22819  ssnei2  23071  t1ficld  23282  t1sep2  23324  unconn  23384  1stcclb  23399  ptbasfi  23536  tx1stc  23605  qtoptop2  23654  r0sep  23703  ustincl  24163  ustdiag  24164  ustinvel  24165  ustexhalf  24166  psmet0  24264  psmettri2  24265  prdsdsf  24323  prdsxmet  24325  cncfi  24857  ovolfiniun  25473  mbfimaopnlem  25627  limciun  25866  dvcn  25894  dvmptfsum  25950  dvfsumle  25997  dvfsumleOLD  25998  dvfsumabs  26000  dvfsumlem3  26006  itgsubst  26027  fsumvma  27194  dchrelbasd  27220  dchrisumlem3  27472  sssslt1  27777  sssslt2  27778  madeval2  27829  elmade  27843  axcontlem9  28918  usgruspgrb  29129  uspgrloopvtxel  29463  umgr2v2evtxel  29469  clwwlknonex2lem2  30056  3spthd  30124  grpoass  30451  lnolin  30702  elnlfn  31876  strlem4  32202  hstrlem4  32210  atmd  32347  nn0min  32767  omndadd  33027  slmdlema  33153  qsxpid  33330  esumcvg  34062  measxun2  34186  sibfima  34315  bnj110  34847  bnj594  34901  bnj1491  35046  loop1cycl  35117  cvmcov  35243  mrsubcn  35499  dfon2lem5  35763  ifscgr  36020  nn0prpw  36299  neibastop2lem  36336  bj-restb  37070  poimirlem25  37627  poimirlem32  37634  mbfresfi  37648  totbndss  37759  ghomlinOLD  37870  rngodi  37886  rngodir  37887  rngoass  37888  rngohomadd  37951  rngohommul  37952  crngocom  37983  idladdcl  38001  idllmulcl  38002  idlrmulcl  38003  exlimddvf  38103  oposlem  39158  cvlexch1  39304  hlsuprexch  39358  lautle  40061  elrfirn2  42685  wepwsolem  43032  kelac1  43053  islssfg2  43061  lnmlssfg  43070  onov0suclim  43264  relprel  44944  ovolval5lem3  46641  2elfz3nn0  47301  2elfz2melfz  47303  icceuelpartlem  47395  wtgoldbnnsum4prm  47762  bgoldbnnsum3prm  47764  bgoldbtbnd  47769  oppcendc  48900  setrec2fun  49306