Theorem mpan9 281

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

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  sylan  283  vtocl2gf  2863  vtocl3gf  2864  vtoclegft  2875  sbcthdv  3043  disji2  4075  exmid1stab  4292  swopolem  4396  funssres  5360  fvmptssdm  5721  fmptcof  5804  fliftfuns  5928  isorel  5938  oveqrspc2v  6034  caovclg  6164  caovcomg  6167  caovassg  6170  caovcang  6173  caovordig  6177  caovordg  6179  caovdig  6186  caovdirg  6189  qliftfuns  6774  nneneq  7026  supmoti  7171  exmidonfinlem  7382  recexprlemopl  7823  recexprlemopu  7825  cauappcvgprlemladdrl  7855  caucvgsrlemcl  7987  caucvgsrlemfv  7989  caucvgsr  8000  suplocsrlempr  8005  ltordlem  8640  lble  9105  uz11  9757  seq3caopr3  10725  ccatass  11156  swrdswrd  11252  swrdccatin1  11272  swrdccatin2  11276  climcaucn  11877  sumdc  11884  fsum3  11913  fsumf1o  11916  fsum3cvg2  11920  isummulc2  11952  fsum2dlemstep  11960  fisumcom2  11964  fsumshftm  11971  fisum0diag2  11973  fsum00  11988  isumshft  12016  clim2prod  12065  prodmodclem2  12103  zproddc  12105  fprodseq  12109  fprodf1o  12114  prodssdc  12115  fprodm1s  12127  fprodp1s  12128  fprodcllemf  12139  fprodabs  12142  fprod2dlemstep  12148  fprodcom2fi  12152  dvdsprm  12674  pythagtriplem4  12806  pcmptdvds  12883  lidrididd  13430  grpidinv2  13606  ghmlin  13800  srgrz  13962  srglz  13963  ringinvnz1ne0  14027  rrgeq0i  14243  lmodlema  14271  islmodd  14272  lsslss  14360  ssnei2  14846  psmet0  15016  psmettri2  15017  cncfi  15267  dvcn  15389  dvmptfsum  15414  usgruspgrben  15999  wlk1walkdom  16100  nninfsellemdc  16436