Theorem impel 508

Description: An inference for implication elimination. (Contributed by Giovanni Mascellani, 23-May-2019.) (Proof shortened by Wolf Lammen, 2-Sep-2020.)

Hypotheses

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

Assertion

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

Proof of Theorem impel

Step	Hyp	Ref	Expression
1		impel.2	. . 3 ⊢ (𝜃 → 𝜓)
2		impel.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	imp 409	1 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  equs5e  2477  elabgt  3663  mob2  3706  ssn0rex  4315  reusv2lem2  5292  copsex2t  5376  reuop  6139  trssord  6203  trsuc  6270  funimass2  6432  fvelima  6726  fvmptf  6784  funfvima2  6987  funfvima3  6992  tfi  7562  suppssov1  7856  tposf2  7910  wfrlem4  7952  wfrlem10  7958  ectocld  8358  mapsnd  8444  resixpfo  8494  f1oeng  8522  nneneq  8694  nnsdomg  8771  fiint  8789  fodomfi  8791  eqinf  8942  hartogslem1  9000  cantnf  9150  rankwflemb  9216  carden2a  9389  carduni  9404  harval2  9420  cardaleph  9509  alephval3  9530  dfac5  9548  cfcof  9690  axdc4lem  9871  nqereu  10345  recexsr  10523  seqcoll  13816  swrdswrd  14061  swrdccatin1  14081  swrdccatin2  14085  repswswrd  14140  climcau  15021  odd2np1  15684  lcmfunsnlem2lem2  15977  coprmproddvdslem  16000  dvdsprm  16041  vdwlem6  16316  imasvscafn  16804  dirref  17839  irredn1  19450  isdrngd  19521  gsummoncoe1  20466  psgnghm  20718  prdstopn  22230  cnextcn  22669  tnggrpr  23258  ovolctb  24085  dyadmbl  24195  itg1addlem4  24294  itg1le  24308  dvcnp2  24511  c1liplem1  24587  pserulm  25004  perfectlem2  25800  dchrisumlem2  26060  axlowdimlem16  26737  wlkv0  27426  wlkp1lem1  27449  wlkswwlksf1o  27651  wspniunwspnon  27696  trlsegvdeglem1  27993  frcond4  28043  2clwwlk2clwwlk  28123  opabssi  30358  nn0xmulclb  30490  cusgr3cyclex  32378  satfun  32653  fundmpss  33004  frrlem4  33121  noresle  33195  nn0prpw  33666  bj-restpw  34377  bj-prmoore  34401  domalom  34679  cover2  34983  setindtr  39614  climxlim2lem  42118  2reuimp  43307  fvelsetpreimafv  43540  imasetpreimafvbijlemfo  43558  reupr  43677  lighneallem4  43768  proththd  43772  lincresunit3  44529